let X be non empty TopSpace; :: thesis: ( ( for X0 being SubSpace of X holds not X0 is nowhere_dense ) implies X is almost_discrete )
assume A1: for X0 being SubSpace of X holds not X0 is nowhere_dense ; :: thesis: X is almost_discrete
now :: thesis: for A being non empty Subset of X holds not A is nowhere_dense
let A be non empty Subset of X; :: thesis: not A is nowhere_dense
consider X0 being non empty strict SubSpace of X such that
A2: A = the carrier of X0 by TSEP_1:10;
not X0 is nowhere_dense by A1;
hence not A is nowhere_dense by A2; :: thesis: verum
end;
hence X is almost_discrete by TEX_1:def 6; :: thesis: verum