let X be non trivial TopSpace; :: thesis: for D being non empty proper Subset of X ex Y0 being non empty strict proper SubSpace of X st D = the carrier of Y0
let D be non empty proper Subset of X; :: thesis: ex Y0 being non empty strict proper SubSpace of X st D = the carrier of Y0
consider Y0 being non empty strict SubSpace of X such that
A1: D = the carrier of Y0 by TSEP_1:10;
reconsider Y0 = Y0 as non empty strict proper SubSpace of X by A1, TEX_2:8;
take Y0 ; :: thesis: D = the carrier of Y0
thus D = the carrier of Y0 by A1; :: thesis: verum