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