let Y be non empty TopStruct ; :: thesis: for Y0 being SubSpace of Y
for A being Subset of Y st A = the carrier of Y0 & Y0 is anti-discrete holds
A is anti-discrete
let Y0 be SubSpace of Y; :: thesis: for A being Subset of Y st A = the carrier of Y0 & Y0 is anti-discrete holds
A is anti-discrete
let A be Subset of Y; :: thesis: ( A = the carrier of Y0 & Y0 is anti-discrete implies A is anti-discrete )
assume A1: A = the carrier of Y0 ; :: thesis: ( not Y0 is anti-discrete or A is anti-discrete )
assume Y0 is anti-discrete ; :: thesis: A is anti-discrete
then A2: the topology of Y0 = {{} ,the carrier of Y0} by TDLAT_3:def 2;

now

let G be Subset of Y; :: thesis: ( not G is open or A misses G or A c= G )
assume A3: G is open ; :: thesis: ( A misses G or A c= G )
reconsider H = A /\ G as Subset of Y0 by A1, XBOOLE_1:17;

now

take G = G; :: thesis: ( G in the topology of Y & H = G /\ ([#] Y0) )
thus G in the topology of Y by A3, PRE_TOPC:def 5; :: thesis: H = G /\ ([#] Y0)
thus H = G /\ ([#] Y0) by A1; :: thesis: verum

end;

then H in the topology of Y0 by PRE_TOPC:def 9;
then ( A /\ G = {} or A /\ G = the carrier of Y0 ) by A2, TARSKI:def 2;
hence ( A misses G or A c= G ) by A1, XBOOLE_0:def 7, XBOOLE_1:17; :: thesis: verum

end;

hence A is anti-discrete by Def3; :: thesis: verum