Ga is a path formula, and to discuss it, we need a path to talk about it, right. In my example above for [(EGa) WB (Ga)], I considered the path 0->2->3->3... and Ga holds on that path from state 3 onwards. However, EGa holds on states 0,1,3 and therefore also on state 0, i.e., the first state on that path. That is so, since the path used to justify EGa there is another path, namely, 0->1->1...