let C1, C2 be Subset of GX; :: thesis: ( ( 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 ) ) & ( for p being set st p in the carrier of GX holds
( p in C2 iff for G being Subset of GX st G is open & p in G holds
A meets G ) ) implies C1 = C2 )
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: C1 = C2
for x being object holds
( x in C1 iff x in C2 )

proof

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

proof

assume A4: x in C1 ; :: thesis: x in C2
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: verum

end;

assume A5: x in C2 ; :: thesis: x in C1
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: verum

end;

hence C1 = C2 by TARSKI:2; :: thesis: verum