thus ( A is T_0 implies for a being Point of X st a in A holds
A /\ (MaxADSet a) = {a} ) :: thesis: ( ( for a being Point of X st a in A holds
A /\ (MaxADSet a) = {a} ) implies A is T_0 )
proof
assume A1: A is T_0 ; :: thesis: for a being Point of X st a in A holds
A /\ (MaxADSet a) = {a}
let a be Point of X; :: thesis: ( a in A implies A /\ (MaxADSet a) = {a} )
assume A2: a in A ; :: thesis: A /\ (MaxADSet a) = {a}
assume A3: A /\ (MaxADSet a) <> {a} ; :: thesis: contradiction
{a} c= MaxADSet a by TEX_4:18;
then a in MaxADSet a by ZFMISC_1:31;
then a in A /\ (MaxADSet a) by A2, XBOOLE_0:def 4;
then consider b being object such that
A4: b in A /\ (MaxADSet a) and
A5: b <> a by A3, ZFMISC_1:35;
reconsider b = b as Point of X by A4;
b in A by A4, XBOOLE_0:def 4;
then A6: MaxADSet a misses MaxADSet b by A1, A2, A5;
b in MaxADSet a by A4, XBOOLE_0:def 4;
hence contradiction by A6, TEX_4:21; :: thesis: verum
end;
assume A7: for a being Point of X st a in A holds
A /\ (MaxADSet a) = {a} ; :: thesis: A is T_0
now :: thesis: for a, b being Point of X st a in A & b in A & a <> b holds
not MaxADSet a meets MaxADSet b
let a, b be Point of X; :: thesis: ( a in A & b in A & a <> b implies not MaxADSet a meets MaxADSet b )
assume that
A8: a in A and
A9: b in A ; :: thesis: ( a <> b implies not MaxADSet a meets MaxADSet b )
A10: A /\ (MaxADSet a) = {a} by A7, A8;
A11: A /\ (MaxADSet b) = {b} by A7, A9;
assume A12: a <> b ; :: thesis: not MaxADSet a meets MaxADSet b
assume MaxADSet a meets MaxADSet b ; :: thesis: contradiction
then {a} = {b} by A10, A11, TEX_4:22;
hence contradiction by A12, ZFMISC_1:3; :: thesis: verum
end;
hence A is T_0 ; :: thesis: verum