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

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, Th35; :: thesis: verum

end;

hence X is almost_discrete by TEX_1:def 7; :: thesis: verum