let X be non empty TopSpace; :: thesis: for x, y being Point of X holds
( Cl {x} c= Cl {y} iff meet { G where G is Subset of X : ( G is open & y in G ) } 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 meet { G where G is Subset of X : ( G is open & y in G ) } 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 ) } ;
set FY = { G where G is Subset of X : ( G is open & y in G ) } ;
A1: [#] X in { G where G is Subset of X : ( G is open & x in G ) } ;
thus ( Cl {x} c= Cl {y} implies meet { G where G is Subset of X : ( G is open & y in G ) } c= meet { G where G is Subset of X : ( G is open & x in G ) } ) :: thesis: ( meet { G where G is Subset of X : ( G is open & y in G ) } c= meet { G where G is Subset of X : ( G is open & x in G ) } implies Cl {x} c= Cl {y} )

proof

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

now

let P be set ; :: thesis: ( P in { G where G is Subset of X : ( G is open & x in G ) } implies P in { G where G is Subset of X : ( G is open & y in G ) } )
assume P in { G where G is Subset of X : ( G is open & x in G ) } ; :: thesis: P in { G where G is Subset of X : ( G is open & y in G ) }
then consider G being Subset of X such that
A3: G = P and
A4: G is open and
A5: x in G ;

now

assume not y in G ; :: thesis: contradiction
then {y} misses G by ZFMISC_1:56;
then A6: Cl {y} misses G by A4, TSEP_1:40;
{x} c= Cl {x} by PRE_TOPC:48;
then x in Cl {x} by ZFMISC_1:37;
hence contradiction by A2, A5, A6, XBOOLE_0:3; :: thesis: verum

end;

hence P in { G where G is Subset of X : ( G is open & y in G ) } by A3, A4; :: thesis: verum

end;

then { G where G is Subset of X : ( G is open & x in G ) } c= { G where G is Subset of X : ( G is open & y in G ) } by TARSKI:def 3;
hence meet { G where G is Subset of X : ( G is open & y in G ) } c= meet { G where G is Subset of X : ( G is open & x in G ) } by A1, SETFAM_1:7; :: thesis: verum

end;

assume A7: meet { G where G is Subset of X : ( G is open & y in G ) } c= meet { G where G is Subset of X : ( G is open & x in G ) } ; :: thesis: Cl {x} c= Cl {y}
set G = (Cl {y}) ` ;
assume A8: not Cl {x} c= Cl {y} ; :: thesis: contradiction

now

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

end;

then x in (Cl {y}) ` by SUBSET_1:50;
then (Cl {y}) ` in { G where G is Subset of X : ( G is open & x in G ) } ;
then meet { G where G is Subset of X : ( G is open & x in G ) } c= (Cl {y}) ` by SETFAM_1:4;
then A9: meet { G where G is Subset of X : ( G is open & y in G ) } c= (Cl {y}) ` by A7, XBOOLE_1:1;
{y} c= Cl {y} by PRE_TOPC:48;
then A10: y in Cl {y} by ZFMISC_1:37;
{y} c= MaxADSet y by Th14;
then A11: y in MaxADSet y by ZFMISC_1:37;
MaxADSet y c= meet { G where G is Subset of X : ( G is open & y in G ) } by Th48;
then y in meet { G where G is Subset of X : ( G is open & y in G ) } by A11;
hence contradiction by A9, A10, XBOOLE_0:def 5; :: thesis: verum