let X be non empty TopSpace; :: thesis: for X0 being SubSpace of X
for A being Subset of X st A = the carrier of X0 holds
( X0 is everywhere_dense iff A is everywhere_dense )
let X0 be SubSpace of X; :: thesis: for A being Subset of X st A = the carrier of X0 holds
( X0 is everywhere_dense iff A is everywhere_dense )
let A be Subset of X; :: thesis: ( A = the carrier of X0 implies ( X0 is everywhere_dense iff A is everywhere_dense ) )
assume A1: A = the carrier of X0 ; :: thesis: ( X0 is everywhere_dense iff A is everywhere_dense )
hence ( X0 is everywhere_dense implies A is everywhere_dense ) by Def2; :: thesis: ( A is everywhere_dense implies X0 is everywhere_dense )
assume A is everywhere_dense ; :: thesis: X0 is everywhere_dense
then for B being Subset of X st B = the carrier of X0 holds
B is everywhere_dense by A1;
hence X0 is everywhere_dense by Def2; :: thesis: verum