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
let A be Subset of Y; :: thesis: ( A = the carrier of Y0 & A is anti-discrete implies Y0 is anti-discrete )
assume A2: A = the carrier of Y0 ; :: thesis: ( not A is anti-discrete or Y0 is anti-discrete )
assume A3: A is anti-discrete ; :: thesis: Y0 is anti-discrete
( {} in the topology of Y0 & the carrier of Y0 in the topology of Y0 ) by A1, PRE_TOPC:5, PRE_TOPC:def 1;
then A4: {{} ,the carrier of Y0} c= the topology of Y0 by ZFMISC_1:38;

now

let D be set ; :: 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 9;
reconsider E = E as Subset of Y ;
A8: E is open by A6, PRE_TOPC:def 5;

now

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

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

hence ( C = {} or C = A ) by A2, A7, XBOOLE_0:def 7; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

then the topology of Y0 c= {{} ,the carrier of Y0} by TARSKI:def 3;
then the topology of Y0 = {{} ,the carrier of Y0} by A4, XBOOLE_0:def 10;
hence Y0 is anti-discrete by TDLAT_3:def 2; :: thesis: verum