let Y be TopSpace-like TopStruct ; :: thesis: ( bool the carrier of Y = {{}, the carrier of Y} implies ( 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 ;
A1: the carrier of Y in the topology of Y by PRE_TOPC:def 1;
E c= the topology of Y ;
then A2: {} in the topology of Y by PRE_TOPC:def 1, ZFMISC_1:2;
assume bool the carrier of Y = {{}, the carrier of Y} ; :: thesis: ( Y is discrete & Y is anti-discrete )
hence ( Y is discrete & Y is anti-discrete ) by A2, A1, Th11; :: thesis: verum