thus ( A is maximal_anti-discrete implies ex x being Point of Y st
( x in A & A = MaxADSet x ) ) :: thesis: ( ex x being Point of Y st
( x in A & A = MaxADSet x ) implies A is maximal_anti-discrete )

proof

assume A1: A is maximal_anti-discrete ; :: thesis: ex x being Point of Y st
( x in A & A = MaxADSet x )
then A <> {} by Th15;
then consider x being object such that
A2: x in A by XBOOLE_0:def 1;
reconsider x = x as Point of Y by A2;
take x ; :: thesis: ( x in A & A = MaxADSet x )
thus x in A by A2; :: thesis: A = MaxADSet x
MaxADSet x is maximal_anti-discrete by Th20;
then A3: MaxADSet x is anti-discrete ;
A is anti-discrete by A1;
then A c= MaxADSet x by A2, Th19;
hence A = MaxADSet x by A1, A3; :: thesis: verum

end;

assume ex x being Point of Y st
( x in A & A = MaxADSet x ) ; :: thesis: A is maximal_anti-discrete
hence A is maximal_anti-discrete by Th20; :: thesis: verum