EGa is true at states {s2;s3;s6}, thus AFEGa must include these states at least since all paths starting there already have reached the set EGa={s2;s3;s6} at the initial point of time. Note that Fp holds if p holds now or at any time in the future. The present time is included.