let X be non empty almost_discrete TopSpace; :: thesis: for A being Subset of X st A is maximal_discrete holds
A is dense
let A be Subset of X; :: thesis: ( A is maximal_discrete implies A is dense )
assume A1: A is maximal_discrete ; :: thesis: A is dense
then A2: 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
A3: a in the carrier of X \ (Cl A) by XBOOLE_0:def 1;
reconsider a = a as Point of X by A3;
set B = A \/ {a};
A4: not a in A

proof

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

end;

A5: A c= A \/ {a} by XBOOLE_1:7;
A6: 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 A7: ( x in A or x in {a} ) by XBOOLE_0:def 3;

now

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 consider G being Subset of X such that
A9: G is open and
A10: A /\ G = {x} by A2, Th32;

now

take E = (Cl A) /\ G; :: thesis: ( E is open & (A \/ {a}) /\ E = {x} )
Cl A is open by TDLAT_3:24;
hence E is open by A9, TOPS_1:38; :: thesis: (A \/ {a}) /\ E = {x}
A11: {x} c= E by A10, PRE_TOPC:48, XBOOLE_1:26;
{x} c= A \/ {a} by A5, A8, ZFMISC_1:37;
then A12: {x} c= (A \/ {a}) /\ E by A11, XBOOLE_1:19;
( not a in Cl A & E c= Cl A ) by A3, XBOOLE_0:def 5, XBOOLE_1:17;
then not a in E ;
then {a} misses E by ZFMISC_1:56;
then A13: {a} /\ E = {} by XBOOLE_0:def 7;
A14: A /\ E c= A /\ G by XBOOLE_1:17, XBOOLE_1:26;
(A \/ {a}) /\ E = (A /\ E) \/ ({a} /\ E) by XBOOLE_1:23;
hence (A \/ {a}) /\ E = {x} by A10, A12, A13, A14, XBOOLE_0:def 10; :: thesis: verum

end;

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

end;

suppose A15: 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} )
A16: G = (Cl A) ` ;
hence G is open ; :: thesis: (A \/ {a}) /\ G = {x}
A17: {a} c= G by A3, ZFMISC_1:37;
A c= Cl A by PRE_TOPC:48;
then A misses G by A16, SUBSET_1:44;
then A18: A /\ G = {} by XBOOLE_0:def 7;
(A \/ {a}) /\ G = (A /\ G) \/ ({a} /\ G) by XBOOLE_1:23;
hence (A \/ {a}) /\ G = {x} by A15, A17, A18, 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 A6; :: 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 A4, ZFMISC_1:37; :: thesis: verum

end;

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

end;

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