let T be non empty trivial TopSpace; :: thesis: ( {the carrier of T} is Basis of T & {} is prebasis of T & {{} } is prebasis of T )
set BB = {the carrier of T};
A1: the carrier of T c= the carrier of T ;
A2: the topology of T = bool the carrier of T by Th9;
reconsider BB = {the carrier of T} as Subset-Family of T by A1, ZFMISC_1:37;
consider x being Element of T;
A3: the topology of T = {{} ,{x}} by Th9;
A4: the carrier of T = {x} by Th9;
A5: {} c= bool the carrier of T by XBOOLE_1:2;
A6: {} c= BB by XBOOLE_1:2;
A7: {} c= the carrier of T by XBOOLE_1:2;
reconsider C = {} as Subset-Family of T by XBOOLE_1:2;
the topology of T c= UniCl BB

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in the topology of T or a in UniCl BB )
assume a in the topology of T ; :: thesis: a in UniCl BB
then ( ( a = {x} & union {{x}} = {x} & BB c= BB & BB c= bool the carrier of T ) or a = {} ) by A3, TARSKI:def 2, ZFMISC_1:31;
hence a in UniCl BB by A4, A5, A6, A7, CANTOR_1:def 1, ZFMISC_1:2; :: thesis: verum

end;

hence A8: {the carrier of T} is Basis of T by A2, CANTOR_1:def 2, TOPS_2:78; :: thesis: ( {} is prebasis of T & {{} } is prebasis of T )
A9: {} c= the topology of T by XBOOLE_1:2;
BB c= FinMeetCl C

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in BB or x in FinMeetCl C )
assume x in BB ; :: thesis: x in FinMeetCl C
then x = the carrier of T by TARSKI:def 1;
then Intersect C = x by SETFAM_1:def 10;
hence x in FinMeetCl C by CANTOR_1:def 4; :: thesis: verum

end;

hence {} is prebasis of T by A8, A9, CANTOR_1:def 5, TOPS_2:78; :: thesis: {{} } is prebasis of T
{} c= the carrier of T by XBOOLE_1:2;
then reconsider D = {{} } as Subset-Family of T by ZFMISC_1:37;
A10: D c= the topology of T by A3, ZFMISC_1:12;
BB c= FinMeetCl D

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in BB or x in FinMeetCl D )
assume x in BB ; :: thesis: x in FinMeetCl D
then A11: x = the carrier of T by TARSKI:def 1;
A12: Intersect C = the carrier of T by SETFAM_1:def 10;
C c= D by XBOOLE_1:2;
hence x in FinMeetCl D by A11, A12, CANTOR_1:def 4; :: thesis: verum

end;

hence {{} } is prebasis of T by A8, A10, CANTOR_1:def 5, TOPS_2:78; :: thesis: verum