let T1 be TopSpace; :: thesis: ( T1 is empty implies the topology of T1 = {{} } )
assume T1 is empty ; :: thesis: the topology of T1 = {{} }
then the carrier of T1 = {} ;
then ( the topology of T1 c= {{} } & {} in the topology of T1 ) by PRE_TOPC:def 1, ZFMISC_1:1;
hence the topology of T1 = {{} } by ZFMISC_1:39; :: thesis: verum