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};
the carrier of T in the topology of T by PRE_TOPC:def 1;
then A1: ( B c= the topology of T & {the carrier of T} c= the topology of T ) by CANTOR_1:def 2, ZFMISC_1:37;
then B \/ {the carrier of T} c= the topology of T by XBOOLE_1:8;
then reconsider C = B \/ {the carrier of T} as Subset-Family of T by XBOOLE_1:1;
C is Basis of T

proof

thus C c= the topology of T by A1, XBOOLE_1:8; :: according to CANTOR_1:def 2 :: thesis: the topology of T c= UniCl C
B c= C by XBOOLE_1:7;
then ( UniCl B c= UniCl C & the topology of T c= UniCl B ) by CANTOR_1:9, CANTOR_1:def 2;
hence the topology of T c= UniCl C by XBOOLE_1:1; :: thesis: verum

end;

hence B \/ {the carrier of T} is Basis of T ; :: thesis: verum