let Y be TopStruct ; :: thesis: ( {} in the topology of Y & the carrier of Y in the topology of Y & bool the carrier of Y = {{}, the carrier of Y} implies ( Y is discrete & Y is anti-discrete ) )
assume that
A1: {} in the topology of Y and
A2: the carrier of Y in the topology of Y ; :: thesis: ( not bool the carrier of Y = {{}, the carrier of Y} or ( Y is discrete & Y is anti-discrete ) )
assume A3: bool the carrier of Y = {{}, the carrier of Y} ; :: thesis: ( Y is discrete & Y is anti-discrete )
{{}, the carrier of Y} c= the topology of Y by A1, A2, ZFMISC_1:32;
then the topology of Y = bool the carrier of Y by A3;
hence ( Y is discrete & Y is anti-discrete ) by A3; :: thesis: verum