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} by TDLAT_3:12;

now

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

end;

hence Y is trivial by Def1; :: thesis: verum