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