let GX be TopStruct ; :: thesis: for R being Subset of GX st R is nowhere_dense holds
R ` is dense
let R be Subset of GX; :: thesis: ( R is nowhere_dense implies R ` is dense )
assume R is nowhere_dense ; :: thesis: R ` is dense
then Cl R is boundary by Def5;
then (Cl R) ` is dense by Def4;
then A1: Cl ((Cl R) ` ) = [#] GX by Def3;
R c= Cl R by PRE_TOPC:48;
then (Cl R) ` c= R ` by SUBSET_1:31;
then [#] GX c= Cl (R ` ) by A1, PRE_TOPC:49;
then [#] GX = Cl (R ` ) by XBOOLE_0:def 10;
hence R ` is dense by Def3; :: thesis: verum