let X be non empty TopSpace; :: thesis: for Y0 being anti-discrete SubSpace of X

for X0 being open SubSpace of X holds

( Y0 misses X0 or Y0 is SubSpace of X0 )

let Y0 be anti-discrete SubSpace of X; :: thesis: for X0 being open SubSpace of X holds

( Y0 misses X0 or Y0 is SubSpace of X0 )

reconsider A = the carrier of Y0 as Subset of X by TSEP_1:1;

let X0 be open SubSpace of X; :: thesis: ( Y0 misses X0 or Y0 is SubSpace of X0 )

reconsider G = the carrier of X0 as Subset of X by TSEP_1:1;

A1: G is open by TSEP_1:16;

A is anti-discrete by Th66;

then ( A misses G or A c= G ) by A1;

hence ( Y0 misses X0 or Y0 is SubSpace of X0 ) by TSEP_1:4, TSEP_1:def 3; :: thesis: verum

for X0 being open SubSpace of X holds

( Y0 misses X0 or Y0 is SubSpace of X0 )

let Y0 be anti-discrete SubSpace of X; :: thesis: for X0 being open SubSpace of X holds

( Y0 misses X0 or Y0 is SubSpace of X0 )

reconsider A = the carrier of Y0 as Subset of X by TSEP_1:1;

let X0 be open SubSpace of X; :: thesis: ( Y0 misses X0 or Y0 is SubSpace of X0 )

reconsider G = the carrier of X0 as Subset of X by TSEP_1:1;

A1: G is open by TSEP_1:16;

A is anti-discrete by Th66;

then ( A misses G or A c= G ) by A1;

hence ( Y0 misses X0 or Y0 is SubSpace of X0 ) by TSEP_1:4, TSEP_1:def 3; :: thesis: verum