let T be TopSpace; :: thesis: for U, V being Subset of T
for B being set st U in B & V in B & B \/ {(U \/ V)} is Basis of T holds
B is Basis of T
let U, V be Subset of T; :: thesis: for B being set st U in B & V in B & B \/ {(U \/ V)} is Basis of T holds
B is Basis of T
let B be set ; :: thesis: ( U in B & V in B & B \/ {(U \/ V)} is Basis of T implies B is Basis of T )
assume that
A1: U in B and
A2: V in B and
A3: B \/ {(U \/ V)} is Basis of T ; :: thesis: B is Basis of T
A4: B c= B \/ {(U \/ V)} by XBOOLE_1:7;
then reconsider B9 = B as Subset-Family of T by A3, XBOOLE_1:1;

A5: now :: thesis: for A being Subset of T st A is open holds
for p being Point of T st p in A holds
ex a being Subset of T st
( a in B9 & p in a & a c= A )

A6: V c= U \/ V by XBOOLE_1:7;
A7: U c= U \/ V by XBOOLE_1:7;
let A be Subset of T; :: thesis: ( A is open implies for p being Point of T st p in A holds
ex a being Subset of T st
( a in B9 & p in a & a c= A ) )
assume A8: A is open ; :: thesis: for p being Point of T st p in A holds
ex a being Subset of T st
( a in B9 & p in a & a c= A )
let p be Point of T; :: thesis: ( p in A implies ex a being Subset of T st
( a in B9 & p in a & a c= A ) )
assume p in A ; :: thesis: ex a being Subset of T st
( a in B9 & p in a & a c= A )
then consider A9 being Subset of T such that
A9: A9 in B \/ {(U \/ V)} and
A10: p in A9 and
A11: A9 c= A by A3, A8, YELLOW_9:31;
assume A12: for a being Subset of T holds
( not a in B9 or not p in a or not a c= A ) ; :: thesis: contradiction
( A9 in B or A9 = U \/ V ) by A9, ZFMISC_1:136;
then ( ( p in U & U c= A ) or ( p in V & V c= A ) ) by A10, A11, A12, A7, A6, XBOOLE_0:def 3;
hence contradiction by A1, A2, A12; :: thesis: verum

end;

B \/ {(U \/ V)} c= the topology of T by A3, TOPS_2:64;
hence B is Basis of T by A5, A4, XBOOLE_1:1, YELLOW_9:32; :: thesis: verum