let X be non empty TopSpace; :: thesis: for A being Subset of X holds Int A = union { G where G is Subset of X : ( G is open & G c= A ) }

let A be Subset of X; :: thesis: Int A = union { G where G is Subset of X : ( G is open & G c= A ) }

set F = { G where G is Subset of X : ( G is open & G c= A ) } ;

A1: { G where G is Subset of X : ( G is open & G c= A ) } c= bool the carrier of X

then {} X in { G where G is Subset of X : ( G is open & G c= A ) } ;

then reconsider F = { G where G is Subset of X : ( G is open & G c= A ) } as non empty Subset-Family of X by A1;

Int A c= A by TOPS_1:16;

then Int A in F ;

then A3: Int A c= union F by ZFMISC_1:74;

then union F c= Int A by A2, TOPS_1:24, TOPS_2:19;

hence Int A = union { G where G is Subset of X : ( G is open & G c= A ) } by A3; :: thesis: verum

let A be Subset of X; :: thesis: Int A = union { G where G is Subset of X : ( G is open & G c= A ) }

set F = { G where G is Subset of X : ( G is open & G c= A ) } ;

A1: { G where G is Subset of X : ( G is open & G c= A ) } c= bool the carrier of X

proof

{} c= A
;
let C be object ; :: according to TARSKI:def 3 :: thesis: ( not C in { G where G is Subset of X : ( G is open & G c= A ) } or C in bool the carrier of X )

assume C in { G where G is Subset of X : ( G is open & G c= A ) } ; :: thesis: C in bool the carrier of X

then ex P being Subset of X st

( C = P & P is open & P c= A ) ;

hence C in bool the carrier of X ; :: thesis: verum

end;assume C in { G where G is Subset of X : ( G is open & G c= A ) } ; :: thesis: C in bool the carrier of X

then ex P being Subset of X st

( C = P & P is open & P c= A ) ;

hence C in bool the carrier of X ; :: thesis: verum

then {} X in { G where G is Subset of X : ( G is open & G c= A ) } ;

then reconsider F = { G where G is Subset of X : ( G is open & G c= A ) } as non empty Subset-Family of X by A1;

now :: thesis: for P being set st P in F holds

P c= A

then A2:
union F c= A
by ZFMISC_1:76;P c= A

let P be set ; :: thesis: ( P in F implies P c= A )

assume P in F ; :: thesis: P c= A

then ex G being Subset of X st

( G = P & G is open & G c= A ) ;

hence P c= A ; :: thesis: verum

end;assume P in F ; :: thesis: P c= A

then ex G being Subset of X st

( G = P & G is open & G c= A ) ;

hence P c= A ; :: thesis: verum

Int A c= A by TOPS_1:16;

then Int A in F ;

then A3: Int A c= union F by ZFMISC_1:74;

now :: thesis: for S being Subset of X st S in F holds

S is open

then
F is open
by TOPS_2:def 1;S is open

let S be Subset of X; :: thesis: ( S in F implies S is open )

assume S in F ; :: thesis: S is open

then ex G being Subset of X st

( G = S & G is open & G c= A ) ;

hence S is open ; :: thesis: verum

end;assume S in F ; :: thesis: S is open

then ex G being Subset of X st

( G = S & G is open & G c= A ) ;

hence S is open ; :: thesis: verum

then union F c= Int A by A2, TOPS_1:24, TOPS_2:19;

hence Int A = union { G where G is Subset of X : ( G is open & G c= A ) } by A3; :: thesis: verum