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