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