let Y be TopSpace-like TopStruct ; :: thesis: ( bool the carrier of Y = {{} ,the carrier of Y} implies ( Y is discrete & Y is anti-discrete ) )
assume A1: bool the carrier of Y = {{} ,the carrier of Y} ; :: thesis: ( Y is discrete & Y is anti-discrete )
reconsider E = {} as Subset-Family of Y by XBOOLE_1:2;
reconsider E = E as Subset-Family of Y ;
( E c= the topology of Y & union E = {} ) by XBOOLE_1:2, ZFMISC_1:2;
then ( {} in the topology of Y & the carrier of Y in the topology of Y ) by PRE_TOPC:def 1;
hence ( Y is discrete & Y is anti-discrete ) by A1, Th13; :: thesis: verum