let Y be non empty TopSpace; :: thesis: ( Y is trivial implies ( Y is anti-discrete & Y is discrete ) )
assume Y is trivial ; :: thesis: ( Y is anti-discrete & Y is discrete )
then consider d being Element of Y such that
A1: the carrier of Y = {d} by Def1;
( {} in the topology of Y & the carrier of Y in the topology of Y ) by PRE_TOPC:5, PRE_TOPC:def 1;
then A2: {{} ,the carrier of Y} c= the topology of Y by ZFMISC_1:38;
A3: bool the carrier of Y = {{} ,the carrier of Y} by A1, ZFMISC_1:30;
then the topology of Y = bool the carrier of Y by A2, XBOOLE_0:def 10;
hence ( Y is anti-discrete & Y is discrete ) by A3, TDLAT_3:def 1, TDLAT_3:def 2; :: thesis: verum