let X be non empty almost_discrete TopSpace; :: thesis: 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 )
let Y0 be non empty discrete SubSpace of X; :: thesis: ex X0 being non empty strict SubSpace of X st
( Y0 is SubSpace of X0 & X0 is maximal_discrete )
reconsider A = the carrier of Y0 as Subset of X by TSEP_1:1;
A is discrete by Th20;
then consider M being Subset of X such that
A1: A c= M and
A2: M is maximal_discrete by Th59;
not M is empty by A2, Th40;
then consider X0 being non empty strict SubSpace of X such that
A3: X0 is maximal_discrete and
A4: M = the carrier of X0 by A2, Th47;
take X0 ; :: thesis: ( Y0 is SubSpace of X0 & X0 is maximal_discrete )
thus ( Y0 is SubSpace of X0 & X0 is maximal_discrete ) by A1, A3, A4, TSEP_1:4; :: thesis: verum