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;

( {} in the topology of X & {} c= A ) by PRE_TOPC:5, 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 S be Subset of X; :: thesis: ( S in F implies S is open )
assume S in F ; :: thesis: S is open
then consider G being Subset of X such that
A2: G = S and
A3: G is open and
G c= A ;
thus S is open by A2, A3; :: thesis: verum

end;

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

now

let P be set ; :: thesis: ( P in F implies P c= A )
assume P in F ; :: thesis: P c= A
then consider G being Subset of X such that
A5: G = P and
G is open and
A6: G c= A ;
thus P c= A by A5, A6; :: thesis: verum

end;

then union F c= A by ZFMISC_1:94;
then A7: union F c= Int A by A4, TOPS_1:56, TOPS_2:26;
Int A c= A by TOPS_1:44;
then Int A in F ;
then Int A c= union F by ZFMISC_1:92;
hence Int A = union { G where G is Subset of X : ( G is open & G c= A ) } by A7, XBOOLE_0:def 10; :: thesis: verum