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 set 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 set ; :: 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 )

assume A3: 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 ) } )
V in the topology of T by A1, PRE_TOPC:def 5;
then consider Y being Subset-Family of T such that
A4: Y c= B and
A5: V = union Y by A2, CANTOR_1:def 1;
consider W being set such that
A6: x in W and
A7: W in Y by A3, A5, 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 A6; :: thesis: W in { G where G is Subset of T : ( G in B & G c= V ) }
reconsider G = W as Subset of T by A7;
G c= V by A5, A7, ZFMISC_1:92;
hence W in { G where G is Subset of T : ( G in B & G c= V ) } by A4, A7; :: thesis: verum

end;

given Y being set such that A8: x in Y and
A9: 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 A9;
hence x in V by A8; :: 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