let T be TopSpace; :: thesis: ( T is empty implies ( T is discrete & T is anti-discrete ) )
assume T is empty ; :: thesis: ( T is discrete & T is anti-discrete )
then the carrier of T = {} ;
then bool the carrier of T = {{}, the carrier of T} by ENUMSET1:29, ZFMISC_1:1;
hence ( T is discrete & T is anti-discrete ) by TDLAT_3:14; :: thesis: verum