let Y be non empty TopStruct ; :: thesis: for Y0 being SubSpace of Y st Y0 is TopSpace-like holds
for A being Subset of Y st A = the carrier of Y0 & A is anti-discrete holds
Y0 is anti-discrete
let Y0 be SubSpace of Y; :: thesis: ( Y0 is TopSpace-like implies for A being Subset of Y st A = the carrier of Y0 & A is anti-discrete holds
Y0 is anti-discrete )
assume A1: Y0 is TopSpace-like ; :: thesis: for A being Subset of Y st A = the carrier of Y0 & A is anti-discrete holds
Y0 is anti-discrete
then A2: the carrier of Y0 in the topology of Y0 by PRE_TOPC:def 1;
let A be Subset of Y; :: thesis: ( A = the carrier of Y0 & A is anti-discrete implies Y0 is anti-discrete )
assume A3: A = the carrier of Y0 ; :: thesis: ( not A is anti-discrete or Y0 is anti-discrete )
assume A4: A is anti-discrete ; :: thesis: Y0 is anti-discrete

now :: thesis: for D being object st D in the topology of Y0 holds
D in {{}, the carrier of Y0}

let D be object ; :: thesis: ( D in the topology of Y0 implies D in {{}, the carrier of Y0} )
assume A5: D in the topology of Y0 ; :: thesis: D in {{}, the carrier of Y0}
then reconsider C = D as Subset of Y0 ;
consider E being Subset of Y such that
A6: E in the topology of Y and
A7: C = E /\ ([#] Y0) by A5, PRE_TOPC:def 4;
reconsider E = E as Subset of Y ;
A8: E is open by A6, PRE_TOPC:def 2;

now :: thesis: ( C = {} or C = A )

per cases ( A misses E or A c= E ) by A4, A8;

suppose A misses E ; :: thesis: ( C = {} or C = A )

hence ( C = {} or C = A ) by A3, A7; :: thesis: verum

end;

suppose A c= E ; :: thesis: ( C = {} or C = A )

hence ( C = {} or C = A ) by A3, A7, XBOOLE_1:28; :: thesis: verum

end;

end;

end;

hence D in {{}, the carrier of Y0} by A3, TARSKI:def 2; :: thesis: verum

end;

then A9: the topology of Y0 c= {{}, the carrier of Y0} ;
{} in the topology of Y0 by A1, PRE_TOPC:1;
then {{}, the carrier of Y0} c= the topology of Y0 by A2, ZFMISC_1:32;
then the topology of Y0 = {{}, the carrier of Y0} by A9;
hence Y0 is anti-discrete by TDLAT_3:def 2; :: thesis: verum