let Y be TopStruct ; :: thesis: ( Y is discrete & Y is anti-discrete implies bool the carrier of Y = {{} ,the carrier of Y} )
assume ( Y is discrete & Y is anti-discrete ) ; :: thesis: bool the carrier of Y = {{} ,the carrier of Y}
then ( the topology of Y = bool the carrier of Y & the topology of Y = {{} ,the carrier of Y} ) by Def1, Def2;
hence bool the carrier of Y = {{} ,the carrier of Y} ; :: thesis: verum