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 A1: ( U in B & V in B & B \/ {(U \/ V)} is Basis of T ) ; :: thesis: B is Basis of T
A2: B c= B \/ {(U \/ V)} by XBOOLE_1:7;
then reconsider B' = B as Subset-Family of T by A1, XBOOLE_1:1;
B \/ {(U \/ V)} c= the topology of T by A1, CANTOR_1:def 2;
then A3: B c= the topology of T by A2, XBOOLE_1:1;

now

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 B' & p in a & a c= A ) )
assume A4: A is open ; :: thesis: for p being Point of T st p in A holds
ex a being Subset of T st
( a in B' & 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 B' & p in a & a c= A ) )
assume p in A ; :: thesis: ex a being Subset of T st
( a in B' & p in a & a c= A )
then consider A' being Subset of T such that
A5: ( A' in B \/ {(U \/ V)} & p in A' & A' c= A ) by A1, A4, YELLOW_9:31;
assume A6: for a being Subset of T holds
( not a in B' or not p in a or not a c= A ) ; :: thesis: contradiction
A7: ( U c= U \/ V & V c= U \/ V ) by XBOOLE_1:7;
( A' in B or A' = U \/ V ) by A5, SETWISEO:6;
then ( ( p in U & U c= A ) or ( p in V & V c= A ) ) by A5, A6, A7, XBOOLE_0:def 3, XBOOLE_1:1;
hence contradiction by A1, A6; :: thesis: verum

end;

hence B is Basis of T by A3, YELLOW_9:32; :: thesis: verum