for X being non empty almost_discrete TopSpace
for Y0 being non empty discrete SubSpace of X ex X0 being non empty strict SubSpace of X st
( Y0 is SubSpace of X0 & X0 is maximal_discrete )