let X be non empty TopSpace; :: thesis: for Y0 being non empty T_0 SubSpace of X ex X0 being strict SubSpace of X st
( Y0 is SubSpace of X0 & X0 is maximal_T_0 )
let Y0 be non empty T_0 SubSpace of X; :: thesis: ex X0 being strict SubSpace of X st
( Y0 is SubSpace of X0 & X0 is maximal_T_0 )
reconsider A = the carrier of Y0 as Subset of X by Lm1;
A is T_0 by TSP_1:13;
then consider M being Subset of X such that
A1: A c= M and
A2: M is maximal_T_0 by Th9;
not M is empty by A2, Th4;
then consider X0 being non empty strict SubSpace of X such that
A3: X0 is maximal_T_0 and
A4: M = the carrier of X0 by A2, Th12;
take X0 ; :: thesis: ( Y0 is SubSpace of X0 & X0 is maximal_T_0 )
thus ( Y0 is SubSpace of X0 & X0 is maximal_T_0 ) by A1, A3, A4, TSEP_1:4; :: thesis: verum