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 discrete implies Y1 is 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 discrete or Y1 is discrete )
assume Y0 is discrete ; :: thesis: Y1 is discrete
then the topology of Y0 = bool the carrier of Y0 by TDLAT_3:def 1;
hence Y1 is discrete by A1, TDLAT_3:def 1; :: thesis: verum