let X be non empty TopSpace; :: thesis: for A being Subset of X st A is dense & A is discrete holds
A is maximal_discrete
let A be Subset of X; :: thesis: ( A is dense & A is discrete implies A is maximal_discrete )
assume A1: A is dense ; :: thesis: ( not A is discrete or A is maximal_discrete )
assume A2: A is discrete ; :: thesis: A is maximal_discrete
assume not A is maximal_discrete ; :: thesis: contradiction
then consider D being Subset of X such that
A3: D is discrete and
A4: A c= D and
A5: A <> D by A2;
D \ A <> {} by A4, A5, Lm3;
then consider a being object such that
A6: a in D \ A by XBOOLE_0:def 1;
reconsider a = a as Point of X by A6;
a in D by A6, XBOOLE_0:def 5;
then consider G being Subset of X such that
A7: G is open and
A8: D /\ G = {a} by A3, Th26;
A9: now :: thesis: not A /\ G = {a}
assume A /\ G = {a} ; :: thesis: contradiction
then {a} c= A by XBOOLE_1:17;
then a in A by ZFMISC_1:31;
hence contradiction by A6, XBOOLE_0:def 5; :: thesis: verum
end;
A /\ G c= D /\ G by A4, XBOOLE_1:26;
then ( A /\ G = {} or A /\ G = {a} ) by A8, ZFMISC_1:33;
then ( A misses G or A /\ G = {a} ) ;
then Cl A misses G by A7, A9, TSEP_1:36;
then A10: (Cl A) /\ G = {} ;
now :: thesis: not Cl A = the carrier of X
assume Cl A = the carrier of X ; :: thesis: contradiction
then G = {} by A10, XBOOLE_1:28;
hence contradiction by A8; :: thesis: verum
end;
hence contradiction by A1, TOPS_3:def 2; :: thesis: verum