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

set G = (Cl {y}) ` ;

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

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

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

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:3;

then A9: meet { G where G is Subset of X : ( G is open & y in G ) } c= (Cl {y}) ` by A7;

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

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

{y} c= MaxADSet y by Th12;

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

MaxADSet y c= meet { G where G is Subset of X : ( G is open & y in G ) } by Th46;

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

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

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:6; :: thesis: verum

end;now :: thesis: for P being object st P in { G where G is Subset of X : ( G is open & x in G ) } holds

P in { G where G is Subset of X : ( G is open & y in G ) }

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 ) }
;P in { G where G is Subset of X : ( G is open & y in G ) }

let P be object ; :: 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 ;

end;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 :: thesis: y in G

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

then {y} misses G by ZFMISC_1:50;

then A6: Cl {y} misses G by A4, TSEP_1:36;

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

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

hence contradiction by A2, A5, A6, XBOOLE_0:3; :: thesis: verum

end;then {y} misses G by ZFMISC_1:50;

then A6: Cl {y} misses G by A4, TSEP_1:36;

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

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

hence contradiction by A2, A5, A6, XBOOLE_0:3; :: thesis: verum

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:6; :: thesis: verum

set G = (Cl {y}) ` ;

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

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

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

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:3;

then A9: meet { G where G is Subset of X : ( G is open & y in G ) } c= (Cl {y}) ` by A7;

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

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

{y} c= MaxADSet y by Th12;

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

MaxADSet y c= meet { G where G is Subset of X : ( G is open & y in G ) } by Th46;

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