let Y be 1 -element TopSpace; :: thesis: ( Y is anti-discrete & Y is discrete )
A1: the carrier of Y in the topology of Y by PRE_TOPC:def 1;
ex d being Element of Y st the carrier of Y = {d} by Def1;
then A2: bool the carrier of Y = {{}, the carrier of Y} by ZFMISC_1:24;
{} in the topology of Y by PRE_TOPC:1;
then {{}, the carrier of Y} c= the topology of Y by A1, ZFMISC_1:32;
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 A2; :: thesis: verum