let T be TopSpace; :: thesis: for B being Basis of T holds B \/ { the carrier of T} is Basis of T
let B be Basis of T; :: thesis: B \/ { the carrier of T} is Basis of T
set C = B \/ { the carrier of T};
A1: the carrier of T in the topology of T by PRE_TOPC:def 1;
A2: B c= the topology of T by TOPS_2:64;
A3: { the carrier of T} c= the topology of T by A1, ZFMISC_1:31;
then B \/ { the carrier of T} c= the topology of T by A2, XBOOLE_1:8;
then reconsider C = B \/ { the carrier of T} as Subset-Family of T by XBOOLE_1:1;
A4: C c= the topology of T by A2, A3, XBOOLE_1:8;
A5: UniCl B c= UniCl C by CANTOR_1:9, XBOOLE_1:7;
the topology of T c= UniCl B by CANTOR_1:def 2;
then the topology of T c= UniCl C by A5;
hence B \/ { the carrier of T} is Basis of T by A4, CANTOR_1:def 2, TOPS_2:64; :: thesis: verum