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

now :: thesis: for A being Subset of X st A <> the carrier of X holds
not A is dense

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

now :: thesis: not A is dense

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

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

hence not A is dense by TOPS_3:17; :: thesis: verum

end;

suppose not A is empty ; :: thesis: not A is 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 6;
then reconsider X0 = X0 as strict proper SubSpace of X by A3, TEX_2:8;
not X0 is dense by A1;
hence not A is dense by A3; :: thesis: verum

end;

end;

end;

hence not A is dense ; :: thesis: verum

end;

hence X is discrete by TEX_1:31; :: thesis: verum