let X be non empty non almost_discrete TopSpace; :: thesis: for A0 being non empty proper Subset of X st A0 is dense & A0 is open holds
ex X0 being strict open proper dense SubSpace of X st A0 = the carrier of X0
let A0 be non empty proper Subset of X; :: thesis: ( A0 is dense & A0 is open implies ex X0 being strict open proper dense SubSpace of X st A0 = the carrier of X0 )
assume ( A0 is dense & A0 is open ) ; :: thesis: ex X0 being strict open proper dense SubSpace of X st A0 = the carrier of X0
then consider X0 being non empty strict open dense SubSpace of X such that
A1: A0 = the carrier of X0 by Th23;
reconsider X0 = X0 as strict open proper dense SubSpace of X by A1, TEX_2:8;
take X0 ; :: thesis: A0 = the carrier of X0
thus A0 = the carrier of X0 by A1; :: thesis: verum