let X be non empty non discrete TopSpace; :: thesis: for A0 being non empty Subset of X st A0 is boundary holds
ex X0 being strict boundary SubSpace of X st A0 = the carrier of X0
let A0 be non empty Subset of X; :: thesis: ( A0 is boundary implies ex X0 being strict boundary SubSpace of X st A0 = the carrier of X0 )
assume A0 is boundary ; :: thesis: ex X0 being strict boundary SubSpace of X st A0 = the carrier of X0
then ex X0 being strict SubSpace of X st
( X0 is boundary & A0 = the carrier of X0 ) by Th30;
hence ex X0 being strict boundary SubSpace of X st A0 = the carrier of X0 ; :: thesis: verum