let X be non empty TopSpace; :: thesis: for A being Subset of X st A is everywhere_dense & A is discrete holds
A is open
let A be Subset of X; :: thesis: ( A is everywhere_dense & A is discrete implies A is open )
assume A is everywhere_dense ; :: thesis: ( not A is discrete or A is open )
then A1: Cl (Int A) = the carrier of X by TOPS_3:def 5;
assume A2: A is discrete ; :: thesis: A is open
assume not A is open ; :: thesis: contradiction
then A \ (Int A) <> {} by Lm3, TOPS_1:44;
then consider a being set such that
A3: a in A \ (Int A) by XBOOLE_0:def 1;
reconsider a = a as Point of X by A3;
A \ (Int A) c= A by XBOOLE_1:36;
then consider G being Subset of X such that
A4: G is open and
A5: A /\ G = {a} by A2, A3, Th32;

A6: now

(Int A) /\ G c= {a} by A5, TOPS_1:44, XBOOLE_1:26;
then ( (Int A) /\ G = {} or (Int A) /\ G = {a} ) by ZFMISC_1:39;
then A7: ( Int A misses G or (Int A) /\ G = {a} ) by XBOOLE_0:def 7;

now

assume (Int A) /\ G = {a} ; :: thesis: contradiction
then {a} c= Int A by XBOOLE_1:17;
then a in Int A by ZFMISC_1:37;
hence contradiction by A3, XBOOLE_0:def 5; :: thesis: verum

end;

then Cl (Int A) misses G by A4, A7, TSEP_1:40;
hence (Cl (Int A)) /\ G = {} by XBOOLE_0:def 7; :: thesis: verum

end;

( {a} c= Cl (Int A) & {a} c= G ) by A1, A5, XBOOLE_1:17;
hence contradiction by A6, XBOOLE_1:3, XBOOLE_1:19; :: thesis: verum