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 ;
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
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: A c= A \/ {a} by XBOOLE_1:7;
A5: 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 A6: ( 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 A6, TARSKI:def 1;
suppose A7: 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
A8: G is open and
A9: A /\ G = {x} by A2, Th26;
now :: thesis: ex E being Element of bool the carrier of X st
( E is open & (A \/ {a}) /\ E = {x} )
take E = (Cl A) /\ G; :: thesis: ( E is open & (A \/ {a}) /\ E = {x} )
A10: (A \/ {a}) /\ E = (A /\ E) \/ ({a} /\ E) by XBOOLE_1:23;
Cl A is open by TDLAT_3:22;
hence E is open by A8; :: thesis: (A \/ {a}) /\ E = {x}
A11: {x} c= E by A9, PRE_TOPC:18, XBOOLE_1:26;
E c= Cl A by XBOOLE_1:17;
then not a in E by A3, XBOOLE_0:def 5;
then {a} misses E by ZFMISC_1:50;
then A12: {a} /\ E = {} ;
{x} c= A \/ {a} by A4, A7, ZFMISC_1:31;
then A13: {x} c= (A \/ {a}) /\ E by A11, XBOOLE_1:19;
A /\ E c= A /\ G by XBOOLE_1:17, XBOOLE_1:26;
hence (A \/ {a}) /\ E = {x} by A9, A13, A12, A10; :: thesis: verum
end;
hence ex E being Subset of X st
( E is open & (A \/ {a}) /\ E = {x} ) ; :: thesis: verum
end;
suppose A14: 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} )
A15: (A \/ {a}) /\ G = (A /\ G) \/ ({a} /\ G) by XBOOLE_1:23;
A16: 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 A16, SUBSET_1:24;
then A17: A /\ G = {} ;
{a} c= G by A3, ZFMISC_1:31;
hence (A \/ {a}) /\ G = {x} by A14, A17, A15, 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 A18: not a in A by A3, 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 A5, 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 A18, ZFMISC_1:31, XBOOLE_1:7;
hence A <> A \/ {a} ; :: thesis: verum
end;
hence contradiction by A1; :: thesis: verum