let TS be TopSpace; :: thesis: for P being Subset of TS st P is closed holds
Fr P is nowhere_dense
let P be Subset of TS; :: thesis: ( P is closed implies Fr P is nowhere_dense )
assume P is closed ; :: thesis: Fr P is nowhere_dense
then Fr (P `) is nowhere_dense ;
hence Fr P is nowhere_dense ; :: thesis: verum