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 :: thesis: for G being Subset of Y holds
( not G is open or A misses G or A c= G )
let G be Subset of Y; :: thesis: ( not G is open or A misses G or A c= G )
reconsider H = A /\ G as Subset of Y0 by A1, XBOOLE_1:17;
assume A3: G is open ; :: thesis: ( A misses G or A c= G )
( G in the topology of Y & H = G /\ ([#] Y0) ) by A1, A3, PRE_TOPC:def 2;
then H in the topology of Y0 by PRE_TOPC:def 4;
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_1:17; :: thesis: verum
end;
hence A is anti-discrete ; :: thesis: verum