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

proof

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

end;

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

now

let x be set ; :: thesis: ( x in the carrier of X implies x in MaxADSet M )
A8: M c= MaxADSet M by TEX_4:34;
assume x in the carrier of X ; :: thesis: x in MaxADSet M
then reconsider y = x as Point of ;
consider a being Point of 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:37;
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:32;
{y} c= MaxADSet y by TEX_4:20;
then y in MaxADSet y by ZFMISC_1:37;
hence x in MaxADSet M by A11; :: thesis: verum

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 st b in M holds
M /\ (MaxADSet b) = {b}

proof

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

end;

then M is T_0 by Def2;
hence M is maximal_T_0 by A12, Def5; :: thesis: verum