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 ;
then (Cl R) ` is dense ;
then A1: Cl ((Cl R) `) = [#] GX ;
R c= Cl R by PRE_TOPC:18;
then (Cl R) ` c= R ` by SUBSET_1:12;
then [#] GX c= Cl (R `) by A1, PRE_TOPC:19;
then [#] GX = Cl (R `) ;
hence R ` is dense ; :: thesis: verum