let T be 1 -element 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:31;
set x = the Element of T;
A3: the topology of T = {{},{ the Element of T}} by Th9;
A4: the carrier of T = { the Element of T} by Th9;
A5: {} c= bool the carrier of T ;
A6: {} c= BB ;
A7: {} c= the carrier of T ;
reconsider C = {} as Subset-Family of T by XBOOLE_1:2;
the topology of T c= UniCl BB

proof

let a be object ; :: 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 = { the Element of T} & union {{ the Element of T}} = { the Element of T} & BB c= BB & BB c= bool the carrier of T ) or a = {} ) by A3, TARSKI:def 2, ZFMISC_1:25;
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:64; :: thesis: ( {} is prebasis of T & {{}} is prebasis of T )
A9: {} c= the topology of T ;
BB c= FinMeetCl C

proof

let x be object ; :: 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 9;
hence x in FinMeetCl C by CANTOR_1:def 3; :: thesis: verum

end;

hence {} is prebasis of T by A8, A9, CANTOR_1:def 4, TOPS_2:64; :: thesis: {{}} is prebasis of T
{} c= the carrier of T ;
then reconsider D = {{}} as Subset-Family of T by ZFMISC_1:31;
A10: D c= the topology of T by A3, ZFMISC_1:7;
BB c= FinMeetCl D

proof

let x be object ; :: 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 9;
C c= D ;
hence x in FinMeetCl D by A11, A12, CANTOR_1:def 3; :: thesis: verum

end;

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