let T be TopStruct ; :: thesis: for B being Basis of T
for V being Subset of T st V is open holds
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 st V is open holds
V = union { G where G is Subset of T : ( G in B & G c= V ) }
let V be Subset of T; :: thesis: ( V is open implies V = union { G where G is Subset of T : ( G in B & G c= V ) } )
assume A1: V is open ; :: thesis: 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 ) } ;
A2: the topology of T c= UniCl B by CANTOR_1:def 2;
for x being object holds
( x in V iff ex Y being set st
( x in Y & Y in { G where G is Subset of T : ( G in B & G c= V ) } ) )

proof

let x be object ; :: thesis: ( x in V iff ex Y being set st
( x in Y & Y in { G where G is Subset of T : ( G in B & G c= V ) } ) )

hereby :: thesis: ( ex Y being set st
( x in Y & Y in { G where G is Subset of T : ( G in B & G c= V ) } ) implies x in V )

V in the topology of T by A1;
then consider Y being Subset-Family of T such that
A3: Y c= B and
A4: V = union Y by A2, CANTOR_1:def 1;
assume x in V ; :: thesis: ex W being set st
( x in W & W in { G where G is Subset of T : ( G in B & G c= V ) } )
then consider W being set such that
A5: x in W and
A6: W in Y by A4, TARSKI:def 4;
take W = W; :: thesis: ( x in W & W in { G where G is Subset of T : ( G in B & G c= V ) } )
thus x in W by A5; :: thesis: W in { G where G is Subset of T : ( G in B & G c= V ) }
reconsider G = W as Subset of T by A6;
G c= V by A4, A6, ZFMISC_1:74;
hence W in { G where G is Subset of T : ( G in B & G c= V ) } by A3, A6; :: thesis: verum

end;

given Y being set such that A7: x in Y and
A8: Y in { G where G is Subset of T : ( G in B & G c= V ) } ; :: thesis: x in V
ex G being Subset of T st
( Y = G & G in B & G c= V ) by A8;
hence x in V by A7; :: thesis: verum

end;

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