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