thus ( A is maximal_anti-discrete implies for x being Point of Y st x in A holds
A = MaxADSet x ) by Th29; :: thesis: ( ( for x being Point of Y st x in A holds
A = MaxADSet x ) implies A is maximal_anti-discrete )
consider a being set 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

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;

hence A is maximal_anti-discrete by Def9; :: thesis: verum