let X be non empty TopSpace; :: thesis: for A being Subset of X st A is open & A is maximal_discrete holds
A is dense
let A be Subset of X; :: thesis: ( A is open & A is maximal_discrete implies A is dense )
assume A1: A is open ; :: thesis: ( not A is maximal_discrete or A is dense )
assume A2: A is maximal_discrete ; :: thesis: A is dense
then A3: A is discrete by Def7;
assume not A is dense ; :: thesis: contradiction
then ( Cl A <> the carrier of X & Cl A c= the carrier of X ) by TOPS_3:def 2;
then the carrier of X \ (Cl A) <> {} by Lm3;
then consider a being set such that
A4: a in the carrier of X \ (Cl A) by XBOOLE_0:def 1;
reconsider a = a as Point of X by A4;
set B = A \/ {a};
A5: not a in A

proof

( not a in Cl A & A c= Cl A ) by A4, PRE_TOPC:48, XBOOLE_0:def 5;
hence not a in A ; :: thesis: verum

end;

A6: A c= A \/ {a} by XBOOLE_1:7;
A7: A \/ {a} is discrete

proof

now

let x be Point of X; :: thesis: ( x in A \/ {a} implies ex G being Subset of X st
( G is open & (A \/ {a}) /\ G = {x} ) )
assume x in A \/ {a} ; :: thesis: ex G being Subset of X st
( G is open & (A \/ {a}) /\ G = {x} )
then A8: ( x in A or x in {a} ) by XBOOLE_0:def 3;

now

per cases ( x in A or x = a ) by A8, TARSKI:def 1;

suppose A9: x in A ; :: thesis: ex E being Subset of X st
( E is open & (A \/ {a}) /\ E = {x} )

then consider G being Subset of X such that
A10: G is open and
A11: A /\ G = {x} by A3, Th32;

now

take E = {x}; :: thesis: ( E is open & (A \/ {a}) /\ E = {x} )
thus E is open by A1, A10, A11, TOPS_1:38; :: thesis: (A \/ {a}) /\ E = {x}
{x} c= A \/ {a} by A6, A9, ZFMISC_1:37;
hence (A \/ {a}) /\ E = {x} by XBOOLE_1:28; :: thesis: verum

end;

hence ex E being Subset of X st
( E is open & (A \/ {a}) /\ E = {x} ) ; :: thesis: verum

end;

suppose A12: x = a ; :: thesis: ex G being Subset of X st
( G is open & (A \/ {a}) /\ G = {x} )

now

take G = ([#] X) \ (Cl A); :: thesis: ( G is open & (A \/ {a}) /\ G = {x} )
A13: G = (Cl A) ` ;
hence G is open ; :: thesis: (A \/ {a}) /\ G = {x}
A14: {a} c= G by A4, ZFMISC_1:37;
A c= Cl A by PRE_TOPC:48;
then A misses G by A13, SUBSET_1:44;
then A15: A /\ G = {} by XBOOLE_0:def 7;
(A \/ {a}) /\ G = (A /\ G) \/ ({a} /\ G) by XBOOLE_1:23;
hence (A \/ {a}) /\ G = {x} by A12, A14, A15, XBOOLE_1:28; :: thesis: verum

end;

hence ex G being Subset of X st
( G is open & (A \/ {a}) /\ G = {x} ) ; :: thesis: verum

end;

end;

end;

hence ex G being Subset of X st
( G is open & (A \/ {a}) /\ G = {x} ) ; :: thesis: verum

end;

hence A \/ {a} is discrete by Th37; :: thesis: verum

end;

ex D being Subset of X st
( D is discrete & A c= D & A <> D )

proof

take A \/ {a} ; :: thesis: ( A \/ {a} is discrete & A c= A \/ {a} & A <> A \/ {a} )
thus A \/ {a} is discrete by A7; :: thesis: ( A c= A \/ {a} & A <> A \/ {a} )
thus A c= A \/ {a} by XBOOLE_1:7; :: thesis: A <> A \/ {a}

now

assume A = A \/ {a} ; :: thesis: contradiction
then {a} c= A by XBOOLE_1:7;
hence contradiction by A5, ZFMISC_1:37; :: thesis: verum

end;

hence A <> A \/ {a} ; :: thesis: verum

end;

hence contradiction by A2, Def7; :: thesis: verum