let X be non empty almost_discrete TopSpace; :: thesis: for A being Subset of X st A is discrete holds
ex M being Subset of X st
( A c= M & M is maximal_discrete )
let A be Subset of X; :: thesis: ( A is discrete implies ex M being Subset of X st
( A c= M & M is maximal_discrete ) )
set D = ([#] X) \ (Cl A);
set F = { (Cl {d}) where d is Point of X : d in ([#] X) \ (Cl A) } ;
now :: thesis: for C being object st C in { (Cl {d}) where d is Point of X : d in ([#] X) \ (Cl A) } holds
C in bool the carrier of X
let C be object ; :: thesis: ( C in { (Cl {d}) where d is Point of X : d in ([#] X) \ (Cl A) } implies C in bool the carrier of X )
assume C in { (Cl {d}) where d is Point of X : d in ([#] X) \ (Cl A) } ; :: thesis: C in bool the carrier of X
then ex a being Point of X st
( C = Cl {a} & a in ([#] X) \ (Cl A) ) ;
hence C in bool the carrier of X ; :: thesis: verum
end;
then reconsider F = { (Cl {d}) where d is Point of X : d in ([#] X) \ (Cl A) } as Subset-Family of X by TARSKI:def 3;
assume A1: A is discrete ; :: thesis: ex M being Subset of X st
( A c= M & M is maximal_discrete )
defpred S1[ set , set ] means ( $2 in ([#] X) \ (Cl A) & $2 in $1 );
A2: ([#] X) \ (Cl A) = (Cl A) ` ;
then ([#] X) \ (Cl A) is closed by TDLAT_3:21;
then A3: ([#] X) \ (Cl A) = Cl (([#] X) \ (Cl A)) by PRE_TOPC:22;
A c= Cl A by PRE_TOPC:18;
then A misses ([#] X) \ (Cl A) by A2, SUBSET_1:24;
then A4: A /\ (([#] X) \ (Cl A)) = {} ;
reconsider F = F as Subset-Family of X ;
A5: for S being Subset of X st S in F holds
ex x being Point of X st S1[S,x]
proof
let S be Subset of X; :: thesis: ( S in F implies ex x being Point of X st S1[S,x] )
assume S in F ; :: thesis: ex x being Point of X st S1[S,x]
then consider d being Point of X such that
A6: S = Cl {d} and
A7: d in ([#] X) \ (Cl A) ;
take d ; :: thesis: S1[S,d]
{d} c= Cl {d} by PRE_TOPC:18;
hence S1[S,d] by A6, A7, ZFMISC_1:31; :: thesis: verum
end;
consider f being Function of F, the carrier of X such that
A8: for S being Subset of X st S in F holds
S1[S,f . S] from TEX_2:sch 1(A5);
 set M = A \/ (f .: F);
now :: thesis: for x being object st x in f .: F holds
x in ([#] X) \ (Cl A)
let x be object ; :: thesis: ( x in f .: F implies x in ([#] X) \ (Cl A) )
assume x in f .: F ; :: thesis: x in ([#] X) \ (Cl A)
then ex S being object st
( S in F & S in F & x = f . S ) by FUNCT_2:64;
hence x in ([#] X) \ (Cl A) by A8; :: thesis: verum
end;
then A9: f .: F c= ([#] X) \ (Cl A) by TARSKI:def 3;
([#] X) \ (Cl A) misses Cl A by A2, SUBSET_1:24;
then A10: Cl A misses f .: F by A9, XBOOLE_1:63;
thus ex M being Subset of X st
( A c= M & M is maximal_discrete ) :: thesis: verum
proof
take A \/ (f .: F) ; :: thesis: ( A c= A \/ (f .: F) & A \/ (f .: F) is maximal_discrete )
thus A11: A c= A \/ (f .: F) by XBOOLE_1:7; :: thesis: A \/ (f .: F) is maximal_discrete
for x being Point of X ex a being Point of X st
( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (Cl {x}) = {a} )
proof
let x be Point of X; :: thesis: ex a being Point of X st
( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (Cl {x}) = {a} )
A12: [#] X = (Cl A) \/ (([#] X) \ (Cl A)) by XBOOLE_1:45;
now :: thesis: ex a being Point of X st
( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (Cl {x}) = {a} )
per cases ( x in Cl A or x in ([#] X) \ (Cl A) ) by A12, XBOOLE_0:def 3;
suppose A13: x in Cl A ; :: thesis: ex a being Point of X st
( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (Cl {x}) = {a} )
now :: thesis: ex a being Point of X st
( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (Cl {x}) = {a} )
consider a being Point of X such that
A14: a in A and
A15: A /\ (Cl {x}) = {a} by A1, A13, Th54;
take a = a; :: thesis: ( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (Cl {x}) = {a} )
thus a in A \/ (f .: F) by A11, A14; :: thesis: (A \/ (f .: F)) /\ (Cl {x}) = {a}
{x} c= Cl A by A13, ZFMISC_1:31;
then f .: F misses Cl {x} by A10, TOPS_1:5, XBOOLE_1:63;
then (f .: F) /\ (Cl {x}) = {} ;
then (A \/ (f .: F)) /\ (Cl {x}) = (A /\ (Cl {x})) \/ {} by XBOOLE_1:23;
hence (A \/ (f .: F)) /\ (Cl {x}) = {a} by A15; :: thesis: verum
end;
hence ex a being Point of X st
( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (Cl {x}) = {a} ) ; :: thesis: verum
end;
suppose A16: x in ([#] X) \ (Cl A) ; :: thesis: ex a being Point of X st
( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (Cl {x}) = {a} )
then A17: Cl {x} in F ;
now :: thesis: ex a being Point of X st
( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (Cl {x}) = {a} )
reconsider a = f . (Cl {x}) as Point of X by A17, FUNCT_2:5;
take a = a; :: thesis: ( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (Cl {x}) = {a} )
A18: f .: F c= A \/ (f .: F) by XBOOLE_1:7;
now :: thesis: for y being object st y in (A \/ (f .: F)) /\ (Cl {x}) holds
y in {a}
let y be object ; :: thesis: ( y in (A \/ (f .: F)) /\ (Cl {x}) implies y in {a} )
assume A19: y in (A \/ (f .: F)) /\ (Cl {x}) ; :: thesis: y in {a}
then reconsider z = y as Point of X ;
A20: z in Cl {x} by A19, XBOOLE_0:def 4;
A21: z in A \/ (f .: F) by A19, XBOOLE_0:def 4;
{x} c= ([#] X) \ (Cl A) by A16, ZFMISC_1:31;
then Cl {x} c= ([#] X) \ (Cl A) by A3, PRE_TOPC:19;
then not z in A by A4, A20, XBOOLE_0:def 4;
then z in f .: F by A21, XBOOLE_0:def 3;
then consider C being object such that
A22: C in F and
C in F and
A23: z = f . C by FUNCT_2:64;
reconsider C = C as Subset of X by A22;
consider w being Point of X such that
A24: C = Cl {w} and
w in ([#] X) \ (Cl A) by A22;
Cl {z} = Cl {x} by A20, Th49;
then f . (Cl {w}) = a by A8, A22, A23, A24, Th49;
hence y in {a} by A23, A24, TARSKI:def 1; :: thesis: verum
end;
then A25: (A \/ (f .: F)) /\ (Cl {x}) c= {a} by TARSKI:def 3;
A26: a in f .: F by A17, FUNCT_2:35;
hence a in A \/ (f .: F) by A18; :: thesis: (A \/ (f .: F)) /\ (Cl {x}) = {a}
a in Cl {x} by A8, A17;
then A27: {a} c= Cl {x} by ZFMISC_1:31;
{a} c= A \/ (f .: F) by A18, A26, ZFMISC_1:31;
then {a} c= (A \/ (f .: F)) /\ (Cl {x}) by A27, XBOOLE_1:19;
hence (A \/ (f .: F)) /\ (Cl {x}) = {a} by A25; :: thesis: verum
end;
hence ex a being Point of X st
( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (Cl {x}) = {a} ) ; :: thesis: verum
end;
end;
end;
hence ex a being Point of X st
( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (Cl {x}) = {a} ) ; :: thesis: verum
end;
hence A \/ (f .: F) is maximal_discrete by Th58; :: thesis: verum
end;