let X be non empty TopSpace; :: thesis:
let A be Subset of X; :: thesis:
assume A1: A is open ; :: thesis:
assume A2: A is maximal_discrete ; :: thesis:
then A3: A is discrete ;
assume not A is dense ; :: thesis:
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:

let x be Point of X; :: thesis:
assume x in A \/ {a} ; :: thesis:
then A7: ( x in A or x in {a} ) by XBOOLE_0:def 3;

per cases by A7, TARSKI:def 1;

suppose A8: x in A ; :: thesis:

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

take E = {x}; :: thesis:
thus E is open by A1, A9; :: thesis:
{x} c= A \/ {a} by A5, A8, ZFMISC_1:31;
hence (A \/ {a}) /\ E = {x} by XBOOLE_1:28; :: thesis:

end;

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

end;

suppose A10: x = a ; :: thesis:

take G = ([#] X) \ (Cl A); :: thesis:
A11: (A \/ {a}) /\ G = (A /\ G) \/ ({a} /\ G) by XBOOLE_1:23;
A12: G = (Cl A) ` ;
hence G is open ; :: thesis:
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:

end;

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

end;

end;

end;

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

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 )

take A \/ {a} ; :: thesis:
thus A \/ {a} is discrete by A6, Th31; :: thesis:
thus A c= A \/ {a} by XBOOLE_1:7; :: thesis:
A <> A \/ {a} by A14, ZFMISC_1:31, XBOOLE_1:7;
hence A <> A \/ {a} ; :: thesis:

end;

hence contradiction by A2; :: thesis: