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

{} in the topology of Y0 by A1, PRE_TOPC:1;

then {{}, the carrier of Y0} c= the topology of Y0 by A2, ZFMISC_1:32;

then the topology of Y0 = {{}, the carrier of Y0} by A9;

hence Y0 is anti-discrete by TDLAT_3:def 2; :: thesis: verum

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}

then A9:
the topology of Y0 c= {{}, the carrier of Y0}
;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 A5, PRE_TOPC:def 4;

reconsider E = E as Subset of Y ;

A8: E is open by A6, PRE_TOPC:def 2;

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

end;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 4;

reconsider E = E as Subset of Y ;

A8: E is open by A6, PRE_TOPC:def 2;

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

{} in the topology of Y0 by A1, PRE_TOPC:1;

then {{}, the carrier of Y0} c= the topology of Y0 by A2, ZFMISC_1:32;

then the topology of Y0 = {{}, the carrier of Y0} by A9;

hence Y0 is anti-discrete by TDLAT_3:def 2; :: thesis: verum