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 dense iff A is dense )
let X0 be SubSpace of X; :: thesis: for A being Subset of X st A = the carrier of X0 holds
( X0 is dense iff A is dense )
let A be Subset of X; :: thesis: ( A = the carrier of X0 implies ( X0 is dense iff A is dense ) )
assume A1: A = the carrier of X0 ; :: thesis: ( X0 is dense iff A is dense )
hence ( X0 is dense implies A is dense ) by Def1; :: thesis: ( A is dense implies X0 is dense )
assume A is dense ; :: thesis: X0 is dense
then for B being Subset of X st B = the carrier of X0 holds
B is dense by A1;
hence X0 is dense by Def1; :: thesis: verum