let Y be non empty TopSpace; :: thesis: ( Y is discrete & Y is anti-discrete implies Y is trivial )
assume ( Y is discrete & Y is anti-discrete ) ; :: thesis: Y is trivial
then A3: bool the carrier of Y = {{}, the carrier of Y} ;

now :: thesis: ex d0 being Element of Y st {d0} = the carrier of Y

set d0 = the Element of Y;
take d0 = the Element of Y; :: thesis: {d0} = the carrier of Y
thus {d0} = the carrier of Y by A3, TARSKI:def 2; :: thesis: verum

end;

hence Y is trivial ; :: thesis: verum