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:69;

now

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:39;
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:17;
take T ; :: thesis: ( the carrier of T = the carrier of S & the topology of S is prebasis of T )
( the topology of S c= FinMeetCl the topology of S & FinMeetCl the topology of S c= the topology of T ) by CANTOR_1:1, CANTOR_1:4;
then A3: the topology of S c= the topology of T by XBOOLE_1:1;
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 A3, CANTOR_1:def 5; :: thesis: verum