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 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

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

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} )

then A2: y in MaxADSet y by ZFMISC_1:31;

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

then A3: y in meet FX by A2;

set G = (Cl {y}) ` ;

assume A4: not Cl {x} c= Cl {y} ; :: thesis: contradiction

not x in Cl {y} by A4, TOPS_1:5, ZFMISC_1:31;

then x in (Cl {y}) ` by SUBSET_1:29;

then (Cl {y}) ` in FX ;

then A5: meet FX c= (Cl {y}) ` by SETFAM_1:3;

{y} c= Cl {y} by PRE_TOPC:18;

then y in Cl {y} by ZFMISC_1:31;

hence contradiction by A5, A3, XBOOLE_0:def 5; :: thesis: verum

( 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 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

then reconsider FY = { G where G is Subset of X : ( G is open & y in G ) } as Subset-Family of X ;
let C be object ; :: 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;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

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

then reconsider FX = { G where G is Subset of X : ( G is open & x in G ) } as Subset-Family of X ;
let C be object ; :: 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;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

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

{y} c= MaxADSet y
by Th12;
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 Th51;

(Cl {y}) /\ (meet FY) c= 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; :: thesis: verum

end;then A1: meet FY c= meet FX by Th51;

(Cl {y}) /\ (meet FY) c= 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; :: thesis: verum

then A2: y in MaxADSet y by ZFMISC_1:31;

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

then A3: y in meet FX by A2;

set G = (Cl {y}) ` ;

assume A4: not Cl {x} c= Cl {y} ; :: thesis: contradiction

not x in Cl {y} by A4, TOPS_1:5, ZFMISC_1:31;

then x in (Cl {y}) ` by SUBSET_1:29;

then (Cl {y}) ` in FX ;

then A5: meet FX c= (Cl {y}) ` by SETFAM_1:3;

{y} c= Cl {y} by PRE_TOPC:18;

then y in Cl {y} by ZFMISC_1:31;

hence contradiction by A5, A3, XBOOLE_0:def 5; :: thesis: verum