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 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