let X be non empty TopSpace; :: thesis: for X0 being SubSpace of X holds
( X0 is everywhere_dense iff ex X1 being strict open dense SubSpace of X st X1 is SubSpace of X0 )
let X0 be SubSpace of X; :: thesis: ( X0 is everywhere_dense iff ex X1 being strict open dense SubSpace of X st X1 is SubSpace of X0 )
reconsider A = the carrier of X0 as Subset of X by TSEP_1:1;
thus ( X0 is everywhere_dense implies ex X1 being strict open dense SubSpace of X st X1 is SubSpace of X0 ) :: thesis: ( ex X1 being strict open dense SubSpace of X st X1 is SubSpace of X0 implies X0 is everywhere_dense )
proof
assume X0 is everywhere_dense ; :: thesis: ex X1 being strict open dense SubSpace of X st X1 is SubSpace of X0
then A is everywhere_dense ;
then consider C being Subset of X such that
A1: C c= A and
A2: C is open and
A3: C is dense by TOPS_3:41;
not C is empty by A3, TOPS_3:17;
then consider X1 being non empty strict open dense SubSpace of X such that
A4: C = the carrier of X1 by A2, A3, Th23;
take X1 ; :: thesis: X1 is SubSpace of X0
thus X1 is SubSpace of X0 by A1, A4, TSEP_1:4; :: thesis: verum
end;
given X1 being strict open dense SubSpace of X such that A5: X1 is SubSpace of X0 ; :: thesis: X0 is everywhere_dense
reconsider C = the carrier of X1 as Subset of X by TSEP_1:1;
now :: thesis: ex C being Subset of X st
( C c= A & C is open & C is dense )
take C = C; :: thesis: ( C c= A & C is open & C is dense )
thus ( C c= A & C is open & C is dense ) by A5, Def1, TSEP_1:4, TSEP_1:16; :: thesis: verum
end;
then for A being Subset of X st A = the carrier of X0 holds
A is everywhere_dense by TOPS_3:41;
hence X0 is everywhere_dense ; :: thesis: verum