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 set ; :: 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 by XBOOLE_1:2;
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

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:94;
Int A c= A by TOPS_1:44;
then Int A in F ;
then A3: Int A c= union F by ZFMISC_1:92;

now

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:56, TOPS_2:26;
hence Int A = union { G where G is Subset of X : ( G is open & G c= A ) } by A3, XBOOLE_0:def 10; :: thesis: verum