let Y be TopStruct ; :: thesis: ( Y is anti-discrete implies Y is almost_discrete )
assume Y is anti-discrete ; :: thesis: Y is almost_discrete
then for A being Subset of Y st A in the topology of Y holds
the carrier of Y \ A in the topology of Y by Th15;
hence Y is almost_discrete by Def3; :: thesis: verum