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 Th17;
then consider x being set 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 Th22;
then A3: MaxADSet x is anti-discrete by Def7;
A is anti-discrete by A1, Def7;
then A c= MaxADSet x by A2, Th21;
hence A = MaxADSet x by A1, A3, Def7; :: 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 Th22; :: thesis: verum