let T be non empty TopSpace; :: thesis: for B being Basis of T
for V being Subset of T holds Int V = union { G where G is Subset of T : ( G in B & G c= V ) }
let B be Basis of T; :: thesis: for V being Subset of T holds Int V = union { G where G is Subset of T : ( G in B & G c= V ) }
let V be Subset of T; :: thesis: Int V = union { G where G is Subset of T : ( G in B & G c= V ) }
set X = { G where G is Subset of T : ( G in B & G c= V ) } ;
set Y = { G where G is Subset of T : ( G in B & G c= Int V ) } ;
{ G where G is Subset of T : ( G in B & G c= V ) } = { G where G is Subset of T : ( G in B & G c= Int V ) }

proof

thus { G where G is Subset of T : ( G in B & G c= V ) } c= { G where G is Subset of T : ( G in B & G c= Int V ) } :: according to XBOOLE_0:def 10 :: thesis: { G where G is Subset of T : ( G in B & G c= Int V ) } c= { G where G is Subset of T : ( G in B & G c= V ) }

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { G where G is Subset of T : ( G in B & G c= V ) } or e in { G where G is Subset of T : ( G in B & G c= Int V ) } )
assume e in { G where G is Subset of T : ( G in B & G c= V ) } ; :: thesis: e in { G where G is Subset of T : ( G in B & G c= Int V ) }
then consider G being Subset of T such that
A1: e = G and
A2: G in B and
A3: G c= V ;
G c= Int V by A2, A3, Th10, TOPS_1:24;
hence e in { G where G is Subset of T : ( G in B & G c= Int V ) } by A1, A2; :: thesis: verum

end;

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { G where G is Subset of T : ( G in B & G c= Int V ) } or e in { G where G is Subset of T : ( G in B & G c= V ) } )
assume e in { G where G is Subset of T : ( G in B & G c= Int V ) } ; :: thesis: e in { G where G is Subset of T : ( G in B & G c= V ) }
then consider G being Subset of T such that
A4: ( e = G & G in B ) and
A5: G c= Int V ;
Int V c= V by TOPS_1:16;
then G c= V by A5;
hence e in { G where G is Subset of T : ( G in B & G c= V ) } by A4; :: thesis: verum

end;

hence Int V = union { G where G is Subset of T : ( G in B & G c= V ) } by Th9; :: thesis: verum