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:16;
then consider a being object 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, Th26;
A6: now :: thesis: not (Int A) /\ G = {a}
assume (Int A) /\ G = {a} ; :: thesis: contradiction
then {a} c= Int A by XBOOLE_1:17;
then a in Int A by ZFMISC_1:31;
hence contradiction by A3, XBOOLE_0:def 5; :: thesis: verum
end;
(Int A) /\ G c= {a} by A5, TOPS_1:16, XBOOLE_1:26;
then ( (Int A) /\ G = {} or (Int A) /\ G = {a} ) by ZFMISC_1:33;
then ( Int A misses G or (Int A) /\ G = {a} ) ;
then Cl (Int A) misses G by A4, A6, TSEP_1:36;
then A7: (Cl (Int A)) /\ G = {} ;
{a} c= G by A5, XBOOLE_1:17;
hence contradiction by A1, A7, XBOOLE_1:3, XBOOLE_1:19; :: thesis: verum