let Y0, Y1 be TopStruct ; :: thesis: ( TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) & Y0 is almost_discrete implies Y1 is almost_discrete )
assume A1: TopStruct(# the carrier of Y0, the topology of Y0 #) = TopStruct(# the carrier of Y1, the topology of Y1 #) ; :: thesis: ( not Y0 is almost_discrete or Y1 is almost_discrete )
assume Y0 is almost_discrete ; :: thesis: Y1 is almost_discrete
then for A being Subset of Y0 st A in the topology of Y0 holds
the carrier of Y0 \ A in the topology of Y0 by TDLAT_3:def 3;
hence Y1 is almost_discrete by A1, TDLAT_3:def 3; :: thesis: verum