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 ( {} in the topology of Y & 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 ) )
then A1: {{} ,the carrier of Y} c= the topology of Y by ZFMISC_1:38;
assume bool the carrier of Y = {{} ,the carrier of Y} ; :: thesis: ( Y is discrete & Y is anti-discrete )
then ( the topology of Y = bool the carrier of Y & the topology of Y = {{} ,the carrier of Y} ) by A1, XBOOLE_0:def 10;
hence ( Y is discrete & Y is anti-discrete ) by Def1, Def2; :: thesis: verum