let X be non empty TopSpace; :: thesis: for A being Subset of X st A is T_0 holds
ex M being Subset of X st
( A c= M & M is maximal_T_0 )
let A be Subset of X; :: thesis: ( A is T_0 implies ex M being Subset of X st
( A c= M & M is maximal_T_0 ) )
assume A1: A is T_0 ; :: thesis: ex M being Subset of X st
( A c= M & M is maximal_T_0 )
set D = ([#] X) \ (MaxADSet A);
set F = { (MaxADSet d) where d is Point of X : d in ([#] X) \ (MaxADSet A) } ;
{ (MaxADSet d) where d is Point of X : d in ([#] X) \ (MaxADSet A) } c= bool the carrier of X

proof

now

let C be set ; :: thesis: ( C in { (MaxADSet d) where d is Point of X : d in ([#] X) \ (MaxADSet A) } implies C in bool the carrier of X )
assume C in { (MaxADSet d) where d is Point of X : d in ([#] X) \ (MaxADSet A) } ; :: thesis: C in bool the carrier of X
then consider a being Point of X such that
A2: C = MaxADSet a and
a in ([#] X) \ (MaxADSet A) ;
thus C in bool the carrier of X by A2; :: thesis: verum

end;

hence { (MaxADSet d) where d is Point of X : d in ([#] X) \ (MaxADSet A) } c= bool the carrier of X by TARSKI:def 3; :: thesis: verum

end;

then reconsider F = { (MaxADSet d) where d is Point of X : d in ([#] X) \ (MaxADSet A) } as Subset-Family of X ;
reconsider F = F as Subset-Family of X ;
defpred S₁[ Subset of X, set ] means ( $2 in ([#] X) \ (MaxADSet A) & $2 in $1 );
A3: for S being Subset of X st S in F holds
ex x being Point of X st S₁[S,x]

proof

let S be Subset of X; :: thesis: ( S in F implies ex x being Point of X st S₁[S,x] )
assume S in F ; :: thesis: ex x being Point of X st S₁[S,x]
then consider d being Point of X such that
A4: S = MaxADSet d and
A5: d in ([#] X) \ (MaxADSet A) ;
take d ; :: thesis: S₁[S,d]
{d} c= MaxADSet d by TEX_4:20;
hence S₁[S,d] by A4, A5, ZFMISC_1:37; :: thesis: verum

end;

consider f being Function of F,the carrier of X such that
A6: for S being Subset of X st S in F holds
S₁[S,f . S] from TEX_2:sch 1(A3);
set M = A \/ (f .: F);
A7: f .: F c= ([#] X) \ (MaxADSet A)

proof

now

let x be set ; :: thesis: ( x in f .: F implies x in ([#] X) \ (MaxADSet A) )
assume x in f .: F ; :: thesis: x in ([#] X) \ (MaxADSet A)
then consider S being set such that
A8: S in F and
S in F and
A9: x = f . S by FUNCT_2:115;
thus x in ([#] X) \ (MaxADSet A) by A6, A8, A9; :: thesis: verum

end;

hence f .: F c= ([#] X) \ (MaxADSet A) by TARSKI:def 3; :: thesis: verum

end;

A10: ([#] X) \ (MaxADSet A) = (MaxADSet A) ` ;
then A11: MaxADSet A misses ([#] X) \ (MaxADSet A) by SUBSET_1:44;
then A12: MaxADSet A misses f .: F by A7, XBOOLE_1:63;
A c= MaxADSet A by TEX_4:34;
then A misses ([#] X) \ (MaxADSet A) by A10, SUBSET_1:44;
then A13: A /\ (([#] X) \ (MaxADSet A)) = {} by XBOOLE_0:def 7;
thus ex M being Subset of X st
( A c= M & M is maximal_T_0 ) :: thesis: verum

proof

take A \/ (f .: F) ; :: thesis: ( A c= A \/ (f .: F) & A \/ (f .: F) is maximal_T_0 )
thus A14: A c= A \/ (f .: F) by XBOOLE_1:7; :: thesis: A \/ (f .: F) is maximal_T_0
thus A \/ (f .: F) is maximal_T_0 :: thesis: verum

proof

for x being Point of X ex a being Point of X st
( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (MaxADSet 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)) /\ (MaxADSet x) = {a} )
A15: ( [#] X = (MaxADSet A) \/ (([#] X) \ (MaxADSet A)) & [#] X = the carrier of X ) by XBOOLE_1:45;

now

per cases ( x in MaxADSet A or x in ([#] X) \ (MaxADSet A) ) by A15, XBOOLE_0:def 3;

suppose A16: x in MaxADSet A ; :: thesis: ex a being Point of X st
( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (MaxADSet x) = {a} )

now

x in union { (MaxADSet a) where a is Point of X : a in A } by A16, TEX_4:def 11;
then consider C being set such that
A17: x in C and
A18: C in { (MaxADSet a) where a is Point of X : a in A } by TARSKI:def 4;
consider a being Point of X such that
A19: C = MaxADSet a and
A20: a in A by A18;
A21: MaxADSet a = MaxADSet x by A17, A19, TEX_4:23;
take a = a; :: thesis: ( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (MaxADSet x) = {a} )
thus a in A \/ (f .: F) by A14, A20; :: thesis: (A \/ (f .: F)) /\ (MaxADSet x) = {a}
{x} c= MaxADSet A by A16, ZFMISC_1:37;
then MaxADSet {x} c= MaxADSet A by TEX_4:36;
then MaxADSet x c= MaxADSet A by TEX_4:30;
then f .: F misses MaxADSet x by A12, XBOOLE_1:63;
then (f .: F) /\ (MaxADSet x) = {} by XBOOLE_0:def 7;
then (A \/ (f .: F)) /\ (MaxADSet x) = (A /\ (MaxADSet x)) \/ {} by XBOOLE_1:23;
hence (A \/ (f .: F)) /\ (MaxADSet x) = {a} by A1, A20, A21, Def2; :: thesis: verum

end;

hence ex a being Point of X st
( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (MaxADSet x) = {a} ) ; :: thesis: verum

end;

suppose A22: x in ([#] X) \ (MaxADSet A) ; :: thesis: ex a being Point of X st
( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (MaxADSet x) = {a} )

then A23: MaxADSet x in F ;

now

reconsider a = f . (MaxADSet x) as Point of X by A23, FUNCT_2:7;
take a = a; :: thesis: ( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (MaxADSet x) = {a} )
A24: f .: F c= A \/ (f .: F) by XBOOLE_1:7;
A25: a in f .: F by A23, FUNCT_2:43;
hence a in A \/ (f .: F) by A24; :: thesis: (A \/ (f .: F)) /\ (MaxADSet x) = {a}
a in MaxADSet x by A6, A23;
then ( {a} c= MaxADSet x & {a} c= A \/ (f .: F) ) by A24, A25, ZFMISC_1:37;
then A26: {a} c= (A \/ (f .: F)) /\ (MaxADSet x) by XBOOLE_1:19;
(A \/ (f .: F)) /\ (MaxADSet x) c= {a}

proof

now

let y be set ; :: thesis: ( y in (A \/ (f .: F)) /\ (MaxADSet x) implies y in {a} )
assume A27: y in (A \/ (f .: F)) /\ (MaxADSet x) ; :: thesis: y in {a}
then reconsider z = y as Point of X ;
A28: z in MaxADSet x by A27, XBOOLE_0:def 4;
then A29: MaxADSet z = MaxADSet x by TEX_4:23;

now

assume not MaxADSet x c= ([#] X) \ (MaxADSet A) ; :: thesis: contradiction
then MaxADSet x meets MaxADSet A by A10, SUBSET_1:43;
then A30: MaxADSet x c= MaxADSet A by TEX_4:32;
{x} c= MaxADSet x by TEX_4:20;
then x in MaxADSet x by ZFMISC_1:37;
hence contradiction by A11, A22, A30, XBOOLE_0:3; :: thesis: verum

end;

then A31: not z in A by A13, A28, XBOOLE_0:def 4;
z in A \/ (f .: F) by A27, XBOOLE_0:def 4;
then z in f .: F by A31, XBOOLE_0:def 3;
then consider C being set such that
A32: C in F and
C in F and
A33: z = f . C by FUNCT_2:115;
reconsider C = C as Subset of X by A32;
consider w being Point of X such that
A34: C = MaxADSet w and
w in ([#] X) \ (MaxADSet A) by A32;
z in MaxADSet w by A6, A32, A33, A34;
then f . (MaxADSet w) = a by A29, TEX_4:23;
hence y in {a} by A33, A34, TARSKI:def 1; :: thesis: verum

end;

hence (A \/ (f .: F)) /\ (MaxADSet x) c= {a} by TARSKI:def 3; :: thesis: verum

end;

hence (A \/ (f .: F)) /\ (MaxADSet x) = {a} by A26, XBOOLE_0:def 10; :: thesis: verum

end;

hence ex a being Point of X st
( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (MaxADSet x) = {a} ) ; :: thesis: verum

end;

end;

end;

hence ex a being Point of X st
( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (MaxADSet x) = {a} ) ; :: thesis: verum

end;

hence A \/ (f .: F) is maximal_T_0 by Def6; :: thesis: verum

end;

end;