let X be non empty non trivial TopSpace; :: thesis: ( ( for X0 being proper SubSpace of X holds not X0 is everywhere_dense ) implies X is almost_discrete )
assume A1: for X0 being proper SubSpace of X holds not X0 is everywhere_dense ; :: thesis: X is almost_discrete

now

let A be Subset of X; :: thesis: ( A <> the carrier of X implies not A is everywhere_dense )
assume A2: A <> the carrier of X ; :: thesis: not A is everywhere_dense

now

per cases ( A is empty or not A is empty ) ;

suppose A is empty ; :: thesis: not A is everywhere_dense

hence not A is everywhere_dense by TOPS_3:34; :: thesis: verum

end;

suppose not A is empty ; :: thesis: not A is everywhere_dense

then consider X0 being non empty strict SubSpace of X such that
A3: A = the carrier of X0 by TSEP_1:10;
A is proper by A2, SUBSET_1:def 7;
then reconsider X0 = X0 as strict proper SubSpace of X by A3, TEX_2:13;
not X0 is everywhere_dense by A1;
hence not A is everywhere_dense by A3, Th16; :: thesis: verum

end;

end;

end;

hence not A is everywhere_dense ; :: thesis: verum

end;

hence X is almost_discrete by TEX_1:36; :: thesis: verum