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

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

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

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

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

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

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