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

proof

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;

{} c= A ;
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

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;

then A2: union F c= A by ZFMISC_1:76;
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

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;

then F is open by TOPS_2:def 1;
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