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 ) )
set D = ([#] X) \ (MaxADSet A);
set F = { (MaxADSet d) where d is Point of X : d in ([#] X) \ (MaxADSet A) } ;

now :: thesis: for C being object st C in { (MaxADSet d) where d is Point of X : d in ([#] X) \ (MaxADSet A) } holds
C in bool the carrier of X

let C be object ; :: 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 ex a being Point of X st
( C = MaxADSet a & a in ([#] X) \ (MaxADSet A) ) ;
hence C in bool the carrier of X ; :: thesis: verum

end;

then reconsider F = { (MaxADSet d) where d is Point of X : d in ([#] X) \ (MaxADSet A) } as Subset-Family of X by TARSKI:def 3;
assume A1: A is T_0 ; :: thesis: ex M being Subset of X st
( A c= M & M is maximal_T_0 )
defpred S₁[ Subset of X, set ] means ( $2 in ([#] X) \ (MaxADSet A) & $2 in $1 );
A2: ([#] X) \ (MaxADSet A) = (MaxADSet A) ` ;
then A3: MaxADSet A misses ([#] X) \ (MaxADSet A) by SUBSET_1:24;
A c= MaxADSet A by TEX_4:32;
then A misses ([#] X) \ (MaxADSet A) by A2, SUBSET_1:24;
then A4: A /\ (([#] X) \ (MaxADSet A)) = {} by XBOOLE_0:def 7;
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 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
A6: S = MaxADSet d and
A7: d in ([#] X) \ (MaxADSet A) ;
take d ; :: thesis: S₁[S,d]
{d} c= MaxADSet d by TEX_4:18;
hence S₁[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
S₁[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) \ (MaxADSet A)

let x be object ; :: thesis: ( x in f .: F implies x in ([#] X) \ (MaxADSet A) )
assume x in f .: F ; :: thesis: x in ([#] X) \ (MaxADSet A)
then ex S being object st
( S in F & S in F & x = f . S ) by FUNCT_2:64;
hence x in ([#] X) \ (MaxADSet A) by A8; :: thesis: verum

end;

then f .: F c= ([#] X) \ (MaxADSet A) by TARSKI:def 3;
then A9: MaxADSet A misses f .: F by A3, XBOOLE_1:63;
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 A10: A c= A \/ (f .: F) by XBOOLE_1:7; :: thesis: A \/ (f .: F) is maximal_T_0
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} )
A11: [#] X = (MaxADSet A) \/ (([#] X) \ (MaxADSet A)) by XBOOLE_1:45;

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

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

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

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

{x} c= MaxADSet A by A12, ZFMISC_1:31;
then MaxADSet {x} c= MaxADSet A by TEX_4:34;
then MaxADSet x c= MaxADSet A by TEX_4:28;
then f .: F misses MaxADSet x by A9, XBOOLE_1:63;
then (f .: F) /\ (MaxADSet x) = {} by XBOOLE_0:def 7;
then A13: (A \/ (f .: F)) /\ (MaxADSet x) = (A /\ (MaxADSet x)) \/ {} by XBOOLE_1:23;
x in union { (MaxADSet a) where a is Point of X : a in A } by A12, TEX_4:def 11;
then consider C being set such that
A14: x in C and
A15: 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
A16: C = MaxADSet a and
A17: a in A by A15;
take a = a; :: thesis: ( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (MaxADSet x) = {a} )
thus a in A \/ (f .: F) by A10, A17; :: thesis: (A \/ (f .: F)) /\ (MaxADSet x) = {a}
MaxADSet a = MaxADSet x by A14, A16, TEX_4:21;
hence (A \/ (f .: F)) /\ (MaxADSet x) = {a} by A1, A17, A13; :: 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 A18: 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 A19: MaxADSet x in F ;

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

reconsider a = f . (MaxADSet x) as Point of X by A19, FUNCT_2:5;
take a = a; :: thesis: ( a in A \/ (f .: F) & (A \/ (f .: F)) /\ (MaxADSet x) = {a} )
A20: f .: F c= A \/ (f .: F) by XBOOLE_1:7;

now :: thesis: for y being object st y in (A \/ (f .: F)) /\ (MaxADSet x) holds
y in {a}

let y be object ; :: thesis: ( y in (A \/ (f .: F)) /\ (MaxADSet x) implies y in {a} )
assume A21: y in (A \/ (f .: F)) /\ (MaxADSet x) ; :: thesis: y in {a}
then reconsider z = y as Point of X ;
A22: z in A \/ (f .: F) by A21, XBOOLE_0:def 4;
A23: z in MaxADSet x by A21, XBOOLE_0:def 4;
then A24: MaxADSet z = MaxADSet x by TEX_4:21;

now :: thesis: MaxADSet x c= ([#] X) \ (MaxADSet A)

assume not MaxADSet x c= ([#] X) \ (MaxADSet A) ; :: thesis: contradiction
then MaxADSet x meets MaxADSet A by A2, SUBSET_1:23;
then A25: MaxADSet x c= MaxADSet A by TEX_4:30;
{x} c= MaxADSet x by TEX_4:18;
then x in MaxADSet x by ZFMISC_1:31;
hence contradiction by A3, A18, A25, XBOOLE_0:3; :: thesis: verum

end;

then not z in A by A4, A23, XBOOLE_0:def 4;
then z in f .: F by A22, XBOOLE_0:def 3;
then consider C being object such that
A26: C in F and
C in F and
A27: z = f . C by FUNCT_2:64;
reconsider C = C as Subset of X by A26;
consider w being Point of X such that
A28: C = MaxADSet w and
w in ([#] X) \ (MaxADSet A) by A26;
z in MaxADSet w by A8, A26, A27, A28;
then f . (MaxADSet w) = a by A24, TEX_4:21;
hence y in {a} by A27, A28, TARSKI:def 1; :: thesis: verum

end;

then A29: (A \/ (f .: F)) /\ (MaxADSet x) c= {a} by TARSKI:def 3;
A30: a in f .: F by A19, FUNCT_2:35;
hence a in A \/ (f .: F) by A20; :: thesis: (A \/ (f .: F)) /\ (MaxADSet x) = {a}
a in MaxADSet x by A8, A19;
then A31: {a} c= MaxADSet x by ZFMISC_1:31;
{a} c= A \/ (f .: F) by A20, A30, ZFMISC_1:31;
then {a} c= (A \/ (f .: F)) /\ (MaxADSet x) by A31, XBOOLE_1:19;
hence (A \/ (f .: F)) /\ (MaxADSet x) = {a} by A29, 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 ; :: thesis: verum

end;