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;

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 )

hence
A is anti-discrete
; :: thesis: verum( 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;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