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};
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 5, 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 prebasis of T

proof

thus C c= the topology of T by A1, XBOOLE_1:8; :: according to CANTOR_1:def 5 :: thesis: ex b₁ being Basis of T st b₁ c= FinMeetCl C
B c= C by XBOOLE_1:7;
then ( FinMeetCl B c= FinMeetCl C & FinMeetCl B is Basis of T ) by Th23, CANTOR_1:16;
hence ex b₁ being Basis of T st b₁ c= FinMeetCl C ; :: thesis: verum

end;

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