thus
( A is maximal_anti-discrete implies for x being Point of Y st x in A holds

A = MaxADSet x ) by Th27; :: thesis: ( ( for x being Point of Y st x in A holds

A = MaxADSet x ) implies A is maximal_anti-discrete )

consider a being object such that

A1: a in A by XBOOLE_0:def 1;

reconsider a = a as Point of Y by A1;

assume A2: for x being Point of Y st x in A holds

A = MaxADSet x ; :: thesis: A is maximal_anti-discrete

A = MaxADSet x ) by Th27; :: thesis: ( ( for x being Point of Y st x in A holds

A = MaxADSet x ) implies A is maximal_anti-discrete )

consider a being object such that

A1: a in A by XBOOLE_0:def 1;

reconsider a = a as Point of Y by A1;

assume A2: for x being Point of Y st x in A holds

A = MaxADSet x ; :: thesis: A is maximal_anti-discrete

now :: thesis: ex a being Point of Y st

( a in A & A = MaxADSet a )

hence
A is maximal_anti-discrete
; :: thesis: verum( a in A & A = MaxADSet a )

take a = a; :: thesis: ( a in A & A = MaxADSet a )

thus a in A by A1; :: thesis: A = MaxADSet a

thus A = MaxADSet a by A2, A1; :: thesis: verum

end;thus a in A by A1; :: thesis: A = MaxADSet a

thus A = MaxADSet a by A2, A1; :: thesis: verum