thus ( M is maximal_T_0 implies for x being Point of X ex a being Point of X st
( a in M & M /\ (MaxADSet x) = {a} ) ) :: thesis:

proof

assume A1: M is maximal_T_0 ; :: thesis:
then A2: M is T_0 ;
let x be Point of X; :: thesis:
x in MaxADSet M by A1;
then x in union { (MaxADSet a) where a is Point of X : a in M } by TEX_4:def 11;
then consider C being set such that
A3: x in C and
A4: 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
A5: C = MaxADSet a and
A6: a in M by A4;
MaxADSet a = MaxADSet x by A3, A5, TEX_4:21;
then M /\ (MaxADSet x) = {a} by A2, A6;
hence ex a being Point of X st
( a in M & M /\ (MaxADSet x) = {a} ) by A6; :: thesis:

end;

assume A7: for x being Point of X ex a being Point of X st
( a in M & M /\ (MaxADSet x) = {a} ) ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
A8: M c= MaxADSet M by TEX_4:32;
assume x in the carrier of X ; :: thesis:
then reconsider y = x as Point of X ;
consider a being Point of X such that
A9: a in M and
A10: M /\ (MaxADSet y) = {a} by A7;
{a} c= MaxADSet y by A10, XBOOLE_1:17;
then a in MaxADSet y by ZFMISC_1:31;
then (MaxADSet y) /\ (MaxADSet M) <> {} by A9, A8, XBOOLE_0:def 4;
then MaxADSet y meets MaxADSet M by XBOOLE_0:def 7;
then A11: MaxADSet y c= MaxADSet M by TEX_4:30;
{y} c= MaxADSet y by TEX_4:18;
then y in MaxADSet y by ZFMISC_1:31;
hence x in MaxADSet M by A11; :: thesis:

end;

then the carrier of X c= MaxADSet M by TARSKI:def 3;
then A12: MaxADSet M = the carrier of X by XBOOLE_0:def 10;
for b being Point of X st b in M holds
M /\ (MaxADSet b) = {b}

proof

let b be Point of X; :: thesis:
A13: ex a being Point of X st
( a in M & M /\ (MaxADSet b) = {a} ) by A7;
{b} c= MaxADSet b by TEX_4:18;
then A14: b in MaxADSet b by ZFMISC_1:31;
assume b in M ; :: thesis:
then b in M /\ (MaxADSet b) by A14, XBOOLE_0:def 4;
hence M /\ (MaxADSet b) = {b} by A13, TARSKI:def 1; :: thesis:

end;

then M is T_0 ;
hence M is maximal_T_0 by A12; :: thesis: