The PSX (past-strong-X) and PWX (past-weak-X) are defined such that they check whether their argument formula φ holds on the point of time right before the considered point of time. They differ at the initial point of time: PSXφ is false there, and PWXφ is true there.

Now, consider G((PWX a) <-> a): It means, that (PWX a) <-> a holds at all points of time. At time 0, this means true<->a since PWX a is true there, and at time 1, it means a(0) <-> a(1), and thus a(1) must hold, and so on. Thus, always a(t) holds, and that means Ga holds.