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 ;
reconsider E = E as Subset of Y ;
A8: E is open by ;
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 ; :: thesis: verum
end;
end;
end;
hence D in {{}, the carrier of Y0} by ; :: thesis: verum
end;
then A9: the topology of Y0 c= {{}, the carrier of Y0} ;
{} in the topology of Y0 by ;
then {{}, the carrier of Y0} c= the topology of Y0 by ;
then the topology of Y0 = {{}, the carrier of Y0} by A9;
hence Y0 is anti-discrete by TDLAT_3:def 2; :: thesis: verum