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