let GX be TopStruct ; :: thesis: for R being Subset of GX st R is closed holds
( R is nowhere_dense iff R = Fr R )
let R be Subset of GX; :: thesis: ( R is closed implies ( R is nowhere_dense iff R = Fr R ) )
assume R is closed ; :: thesis: ( R is nowhere_dense iff R = Fr R )
then A1: R = Cl R by PRE_TOPC:22;
hereby :: thesis: ( R = Fr R implies R is nowhere_dense )
assume R is nowhere_dense ; :: thesis: R = Fr R
then Cl R is boundary ;
then (Cl R) ` is dense ;
then Fr R = R /\ ([#] GX) by A1;
hence R = Fr R by XBOOLE_1:28; :: thesis: verum
end;
assume R = Fr R ; :: thesis: R is nowhere_dense
then R = R \ (Int R) by A1, Lm2;
then Int (Cl R) = {} by A1, Th16, XBOOLE_1:38;
then Cl R is boundary by Th48;
hence R is nowhere_dense ; :: thesis: verum