let T be non empty TopSpace; :: thesis: for B being prebasis of T holds B \/ { the carrier of T} is prebasis of T
let B be prebasis of T; :: thesis: B \/ { the carrier of T} is prebasis 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: FinMeetCl B c= FinMeetCl C by CANTOR_1:14, XBOOLE_1:7;
FinMeetCl B is Basis of T by Th23;
hence B \/ { the carrier of T} is prebasis of T by A4, A5, CANTOR_1:def 4, TOPS_2:64; :: thesis: verum