thus ( M is maximal_T_0 implies ( M is T_0 & MaxADSet M = the carrier of X ) ) :: thesis: ( M is T_0 & MaxADSet M = the carrier of X implies M is maximal_T_0 )

proof

assume A1: M is maximal_T_0 ; :: thesis: ( M is T_0 & MaxADSet M = the carrier of X )
hence A2: M is T_0 ; :: thesis: MaxADSet M = the carrier of X
the carrier of X c= MaxADSet M

proof

assume not the carrier of X c= MaxADSet M ; :: thesis: contradiction
then consider x being object such that
A3: x in the carrier of X and
A4: not x in MaxADSet M by TARSKI:def 3;
reconsider x = x as Point of X by A3;
set A = M \/ {x};
for a being Point of X st a in M \/ {x} holds
(M \/ {x}) /\ (MaxADSet a) = {a}

proof

let a be Point of X; :: thesis: ( a in M \/ {x} implies (M \/ {x}) /\ (MaxADSet a) = {a} )
assume a in M \/ {x} ; :: thesis: (M \/ {x}) /\ (MaxADSet a) = {a}
then A5: ( a in M or a in {x} ) by XBOOLE_0:def 3;

now :: thesis: (M \/ {x}) /\ (MaxADSet a) = {a}

per cases ( a in M or a = x ) by A5, TARSKI:def 1;

suppose A6: a in M ; :: thesis: (M \/ {x}) /\ (MaxADSet a) = {a}

{x} /\ (MaxADSet a) = {}

proof

assume {x} /\ (MaxADSet a) <> {} ; :: thesis: contradiction
then {x} meets MaxADSet a by XBOOLE_0:def 7;
then A7: x in MaxADSet a by ZFMISC_1:50;
{a} c= M by A6, ZFMISC_1:31;
then MaxADSet {a} c= MaxADSet M by TEX_4:31;
then MaxADSet a c= MaxADSet M by TEX_4:28;
hence contradiction by A4, A7; :: thesis: verum

end;

then (M \/ {x}) /\ (MaxADSet a) = (M /\ (MaxADSet a)) \/ {} by XBOOLE_1:23
.= M /\ (MaxADSet a) ;
hence (M \/ {x}) /\ (MaxADSet a) = {a} by A2, A6; :: thesis: verum

end;

suppose A8: a = x ; :: thesis: (M \/ {x}) /\ (MaxADSet a) = {a}

then A9: {x} c= MaxADSet a by TEX_4:18;
M /\ (MaxADSet a) = {}

proof

A10: M c= MaxADSet M by TEX_4:32;
assume M /\ (MaxADSet a) <> {} ; :: thesis: contradiction
then (MaxADSet a) /\ (MaxADSet M) <> {} by A10, XBOOLE_1:3, XBOOLE_1:26;
then MaxADSet a meets MaxADSet M by XBOOLE_0:def 7;
then A11: MaxADSet a c= MaxADSet M by TEX_4:30;
x in MaxADSet a by A9, ZFMISC_1:31;
hence contradiction by A4, A11; :: thesis: verum

end;

then (M \/ {x}) /\ (MaxADSet a) = {} \/ ({x} /\ (MaxADSet a)) by XBOOLE_1:23
.= {x} /\ (MaxADSet a) ;
hence (M \/ {x}) /\ (MaxADSet a) = {a} by A8, TEX_4:18, XBOOLE_1:28; :: thesis: verum

end;

end;

end;

hence (M \/ {x}) /\ (MaxADSet a) = {a} ; :: thesis: verum

end;

then A12: M \/ {x} is T_0 ;
A13: M c= MaxADSet M by TEX_4:32;
A14: {x} c= M \/ {x} by XBOOLE_1:7;
M c= M \/ {x} by XBOOLE_1:7;
then M = M \/ {x} by A1, A12;
then x in M by A14, ZFMISC_1:31;
hence contradiction by A4, A13; :: thesis: verum

end;

hence MaxADSet M = the carrier of X by XBOOLE_0:def 10; :: thesis: verum

end;

assume A15: M is T_0 ; :: thesis: ( not MaxADSet M = the carrier of X or M is maximal_T_0 )
assume A16: MaxADSet M = the carrier of X ; :: thesis: M is maximal_T_0
for D being Subset of X st D is T_0 & M c= D holds
M = D

proof

let D be Subset of X; :: thesis: ( D is T_0 & M c= D implies M = D )
assume A17: D is T_0 ; :: thesis: ( not M c= D or M = D )
assume A18: M c= D ; :: thesis: M = D
D c= M

proof

assume not D c= M ; :: thesis: contradiction
then consider x being object such that
A19: x in D and
A20: not x in M by TARSKI:def 3;
A21: x in the carrier of X by A19;
reconsider x = x as Point of X by A19;
x in union { (MaxADSet a) where a is Point of X : a in M } by A16, A21, TEX_4:def 11;
then consider C being set such that
A22: x in C and
A23: C in { (MaxADSet a) where a is Point of X : a in M } by TARSKI:def 4;
consider a being Point of X such that
A24: C = MaxADSet a and
A25: a in M by A23;
M /\ (MaxADSet x) c= D /\ (MaxADSet x) by A18, XBOOLE_1:26;
then A26: M /\ (MaxADSet x) c= {x} by A17, A19;
MaxADSet a = MaxADSet x by A22, A24, TEX_4:21;
then M /\ (MaxADSet x) = {a} by A15, A25;
hence contradiction by A20, A25, A26, ZFMISC_1:18; :: thesis: verum

end;

hence M = D by A18, XBOOLE_0:def 10; :: thesis: verum

end;

hence M is maximal_T_0 by A15; :: thesis: verum