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 ) } ;
A1: Cl {x} = meet { F where F is Subset of X : ( F is closed & {x} c= F ) } by Th1;

now

let P be set ; :: 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
A2: F = P and
A3: F is closed and
A4: x in F ;
{x} c= F by A4, ZFMISC_1:37;
hence P in { F where F is Subset of X : ( F is closed & {x} c= F ) } by A2, A3; :: thesis: verum

end;

then A5: { 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 ) } by TARSKI:def 3;

now

let P be set ; :: 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
A6: F = P and
A7: F is closed and
A8: {x} c= F ;
x in F by A8, ZFMISC_1:37;
hence P in { F where F is Subset of X : ( F is closed & x in F ) } by A6, A7; :: thesis: verum

end;

then { 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 ) } by TARSKI:def 3;
hence Cl {x} = meet { F where F is Subset of X : ( F is closed & x in F ) } by A1, A5, XBOOLE_0:def 10; :: thesis: verum