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 ;
assume not A is dense ; :: thesis: contradiction
then Cl A <> the carrier of X by TOPS_3:def 2;
then the carrier of X \ (Cl A) <> {} by Lm3;
then consider a being object 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: A c= A \/ {a} by XBOOLE_1:7;

A6: now :: thesis: for x being Point of X st x in A \/ {a} holds
ex G being Subset of X st
( G is open & (A \/ {a}) /\ G = {x} )

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 A7: ( x in A or x in {a} ) by XBOOLE_0:def 3;

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

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

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

then A9: ex G being Subset of X st
( G is open & A /\ G = {x} ) by A3, Th26;

now :: thesis: ex E being Element of bool the carrier of X st
( E is open & (A \/ {a}) /\ E = {x} )

take E = {x}; :: thesis: ( E is open & (A \/ {a}) /\ E = {x} )
thus E is open by A1, A9; :: thesis: (A \/ {a}) /\ E = {x}
{x} c= A \/ {a} by A5, A8, ZFMISC_1:31;
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 A10: x = a ; :: thesis: ex G being Subset of X st
( G is open & (A \/ {a}) /\ G = {x} )

now :: thesis: ex G being Element of bool the carrier of X st
( G is open & (A \/ {a}) /\ G = {x} )

take G = ([#] X) \ (Cl A); :: thesis: ( G is open & (A \/ {a}) /\ G = {x} )
A11: (A \/ {a}) /\ G = (A /\ G) \/ ({a} /\ G) by XBOOLE_1:23;
A12: G = (Cl A) ` ;
hence G is open ; :: thesis: (A \/ {a}) /\ G = {x}
A c= Cl A by PRE_TOPC:18;
then A misses G by A12, SUBSET_1:24;
then A13: A /\ G = {} ;
{a} c= G by A4, ZFMISC_1:31;
hence (A \/ {a}) /\ G = {x} by A10, A13, A11, 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;

A c= Cl A by PRE_TOPC:18;
then A14: not a in A by A4, XBOOLE_0:def 5;
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 A6, Th31; :: thesis: ( A c= A \/ {a} & A <> A \/ {a} )
thus A c= A \/ {a} by XBOOLE_1:7; :: thesis: A <> A \/ {a}
A <> A \/ {a} by A14, ZFMISC_1:31, XBOOLE_1:7;
hence A <> A \/ {a} ; :: thesis: verum

end;

hence contradiction by A2; :: thesis: verum