let X be non empty TopSpace; :: thesis: for A0 being non empty Subset of X st A0 is maximal_T_0 holds
ex X0 being non empty strict SubSpace of X st
( X0 is maximal_T_0 & A0 = the carrier of X0 )
let A0 be non empty Subset of X; :: thesis: ( A0 is maximal_T_0 implies ex X0 being non empty strict SubSpace of X st
( X0 is maximal_T_0 & A0 = the carrier of X0 ) )
assume A1: A0 is maximal_T_0 ; :: thesis: ex X0 being non empty strict SubSpace of X st
( X0 is maximal_T_0 & A0 = the carrier of X0 )
consider X0 being non empty strict SubSpace of X such that
A2: A0 = the carrier of X0 by TSEP_1:10;
take X0 ; :: thesis: ( X0 is maximal_T_0 & A0 = the carrier of X0 )
thus ( X0 is maximal_T_0 & A0 = the carrier of X0 ) by A1, A2; :: thesis: verum