let X be non empty TopSpace; :: thesis: for x being Point of X holds Cl {x} = meet { F where F is Subset of X : ( F is closed & x in F ) }
let x be Point of X; :: thesis: Cl {x} = meet { F where F is Subset of X : ( F is closed & x in F ) }
set G = { F where F is Subset of X : ( F is closed & x in F ) } ;
set H = { F where F is Subset of X : ( F is closed & {x} c= F ) } ;
now :: thesis: for P being object st P in { F where F is Subset of X : ( F is closed & x in F ) } holds
P in { F where F is Subset of X : ( F is closed & {x} c= F ) }
let P be object ; :: thesis: ( P in { F where F is Subset of X : ( F is closed & x in F ) } implies P in { F where F is Subset of X : ( F is closed & {x} c= F ) } )
assume P in { F where F is Subset of X : ( F is closed & x in F ) } ; :: thesis: P in { F where F is Subset of X : ( F is closed & {x} c= F ) }
then consider F being Subset of X such that
A1: F = P and
A2: F is closed and
A3: x in F ;
{x} c= F by A3, ZFMISC_1:31;
hence P in { F where F is Subset of X : ( F is closed & {x} c= F ) } by A1, A2; :: thesis: verum
end;
then A4: { F where F is Subset of X : ( F is closed & x in F ) } c= { F where F is Subset of X : ( F is closed & {x} c= F ) } ;
now :: thesis: for P being object st P in { F where F is Subset of X : ( F is closed & {x} c= F ) } holds
P in { F where F is Subset of X : ( F is closed & x in F ) }
let P be object ; :: thesis: ( P in { F where F is Subset of X : ( F is closed & {x} c= F ) } implies P in { F where F is Subset of X : ( F is closed & x in F ) } )
assume P in { F where F is Subset of X : ( F is closed & {x} c= F ) } ; :: thesis: P in { F where F is Subset of X : ( F is closed & x in F ) }
then consider F being Subset of X such that
A5: F = P and
A6: F is closed and
A7: {x} c= F ;
x in F by A7, ZFMISC_1:31;
hence P in { F where F is Subset of X : ( F is closed & x in F ) } by A5, A6; :: thesis: verum
end;
then A8: { F where F is Subset of X : ( F is closed & {x} c= F ) } c= { F where F is Subset of X : ( F is closed & x in F ) } ;
Cl {x} = meet { F where F is Subset of X : ( F is closed & {x} c= F ) } by Th1;
hence Cl {x} = meet { F where F is Subset of X : ( F is closed & x in F ) } by A4, A8, XBOOLE_0:def 10; :: thesis: verum