let C1, C2 be Subset of GX; :: thesis:
assume that
A2: for p being set st p in the carrier of GX holds
( p in C1 iff for G being Subset of GX st G is open & p in G holds
A meets G ) and
A3: for p being set st p in the carrier of GX holds
( p in C2 iff for V being Subset of GX st V is open & p in V holds
A meets V ) ; :: thesis:
for x being object holds
( x in C1 iff x in C2 )

let x be object ; :: thesis:
thus ( x in C1 implies x in C2 ) :: thesis:

assume A4: x in C1 ; :: thesis:
then for G being Subset of GX st G is open & x in G holds
A meets G by A2;
hence x in C2 by A3, A4; :: thesis:

end;

assume A5: x in C2 ; :: thesis:
then for V being Subset of GX st V is open & x in V holds
A meets V by A3;
hence x in C1 by A2, A5; :: thesis:

end;