let X be non empty TopSpace; :: thesis: for x, y being Point of X holds
( Cl {x} c= Cl {y} iff MaxADSet y c= meet { G where G is Subset of X : ( G is open & x in G ) } )
let x, y be Point of X; :: thesis: ( Cl {x} c= Cl {y} iff MaxADSet y c= meet { G where G is Subset of X : ( G is open & x in G ) } )
set FX = { G where G is Subset of X : ( G is open & x in G ) } ;
{ G where G is Subset of X : ( G is open & x in G ) } c= bool the carrier of X

proof

let C be set ; :: according to TARSKI:def 3 :: thesis: ( not C in { G where G is Subset of X : ( G is open & x in G ) } or C in bool the carrier of X )
assume C in { G where G is Subset of X : ( G is open & x in G ) } ; :: thesis: C in bool the carrier of X
then ex P being Subset of X st
( C = P & P is open & x in P ) ;
hence C in bool the carrier of X ; :: thesis: verum

end;

then reconsider FX = { G where G is Subset of X : ( G is open & x in G ) } as Subset-Family of X ;
set FY = { G where G is Subset of X : ( G is open & y in G ) } ;
{ G where G is Subset of X : ( G is open & y in G ) } c= bool the carrier of X

proof

let C be set ; :: according to TARSKI:def 3 :: thesis: ( not C in { G where G is Subset of X : ( G is open & y in G ) } or C in bool the carrier of X )
assume C in { G where G is Subset of X : ( G is open & y in G ) } ; :: thesis: C in bool the carrier of X
then ex P being Subset of X st
( C = P & P is open & y in P ) ;
hence C in bool the carrier of X ; :: thesis: verum

end;

then reconsider FY = { G where G is Subset of X : ( G is open & y in G ) } as Subset-Family of X ;
thus ( Cl {x} c= Cl {y} implies MaxADSet y c= meet { G where G is Subset of X : ( G is open & x in G ) } ) :: thesis: ( MaxADSet y c= meet { G where G is Subset of X : ( G is open & x in G ) } implies Cl {x} c= Cl {y} )

proof

assume Cl {x} c= Cl {y} ; :: thesis: MaxADSet y c= meet { G where G is Subset of X : ( G is open & x in G ) }
then A1: meet FY c= meet FX by Th53;
( (Cl {y}) /\ (meet FY) c= meet FY & MaxADSet y = (Cl {y}) /\ (meet FY) ) by XBOOLE_1:17;
hence MaxADSet y c= meet { G where G is Subset of X : ( G is open & x in G ) } by A1, XBOOLE_1:1; :: thesis: verum

end;

assume A2: MaxADSet y c= meet { G where G is Subset of X : ( G is open & x in G ) } ; :: thesis: Cl {x} c= Cl {y}
assume A3: not Cl {x} c= Cl {y} ; :: thesis: contradiction

A4: now

assume x in Cl {y} ; :: thesis: contradiction
then {x} c= Cl {y} by ZFMISC_1:37;
hence contradiction by A3, TOPS_1:31; :: thesis: verum

end;

set G = (Cl {y}) ` ;
( x in (Cl {y}) ` & (Cl {y}) ` is open ) by A4, SUBSET_1:50;
then (Cl {y}) ` in FX ;
then A5: meet FX c= (Cl {y}) ` by SETFAM_1:4;
{y} c= MaxADSet y by Th14;
then y in MaxADSet y by ZFMISC_1:37;
then A6: y in meet FX by A2;
{y} c= Cl {y} by PRE_TOPC:48;
then y in Cl {y} by ZFMISC_1:37;
hence contradiction by A5, A6, XBOOLE_0:def 5; :: thesis: verum