let Y be TopStruct ; :: thesis: ( Y is discrete implies Y is almost_discrete )
assume Y is 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 Th14;
hence Y is almost_discrete by Def3; :: thesis: verum