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:33; :: thesis: verum