let x be Point of T; :: thesis:
thus ex W being Subset of T st
( x in W & W is open & { V where V is Subset of T : ( V in FX & V meets W ) } is finite ) :: thesis:

consider Y being Subset of T such that
A3: x in Y and
A4: Y is open and
A5: { X where X is Subset of T : ( X in GX & X meets Y ) } is finite by A2;
take W = Y; :: thesis:
thus x in W by A3; :: thesis:
thus W is open by A4; :: thesis:
{ V where V is Subset of T : ( V in FX & V meets W ) } c= { X where X is Subset of T : ( X in GX & X meets Y ) }

let Z be object ; :: according to TARSKI:def 3 :: thesis:
assume A6: Z in { V where V is Subset of T : ( V in FX & V meets W ) } ; :: thesis:
ex X being Subset of T st
( Z = X & X in GX & X meets Y )

consider V being Subset of T such that
A7: Z = V and
A8: V in FX and
A9: V meets W by A6;
take X = V; :: thesis:
thus Z = X by A7; :: thesis:
thus X in GX by A1, A8; :: thesis:
thus X meets Y by A9; :: thesis:

end;

hence Z in { X where X is Subset of T : ( X in GX & X meets Y ) } ; :: thesis:

end;

end;