let S be TopStruct ; :: thesis: ex T being strict TopSpace st
( the carrier of T = the carrier of S & the topology of S is prebasis of T )
set T = TopStruct(# the carrier of S,(UniCl (FinMeetCl the topology of S)) #);
A1: {{},{}} = {{}} by ENUMSET1:29;

now :: thesis: ( the carrier of S = {} implies TopStruct(# the carrier of S,(UniCl (FinMeetCl the topology of S)) #) is discrete TopStruct )

assume A2: the carrier of S = {} ; :: thesis: TopStruct(# the carrier of S,(UniCl (FinMeetCl the topology of S)) #) is discrete TopStruct
then ( the topology of S = {} or the topology of S = {{}} ) by ZFMISC_1:1, ZFMISC_1:33;
then FinMeetCl the topology of S = {{}} by A1, A2, Th11, Th17;
then UniCl (FinMeetCl the topology of S) = {{}} by A1, Th11;
hence TopStruct(# the carrier of S,(UniCl (FinMeetCl the topology of S)) #) is discrete TopStruct by A2, TDLAT_3:def 1, ZFMISC_1:1; :: thesis: verum

end;

then reconsider T = TopStruct(# the carrier of S,(UniCl (FinMeetCl the topology of S)) #) as strict TopSpace by CANTOR_1:15;
take T ; :: thesis: ( the carrier of T = the carrier of S & the topology of S is prebasis of T )
A3: the topology of S c= FinMeetCl the topology of S by CANTOR_1:4;
FinMeetCl the topology of S c= the topology of T by CANTOR_1:1;
then A4: the topology of S c= the topology of T by A3;
FinMeetCl the topology of S is Basis of T by Th22;
hence ( the carrier of T = the carrier of S & the topology of S is prebasis of T ) by A4, CANTOR_1:def 4, TOPS_2:64; :: thesis: verum