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 )

( x in A & A = MaxADSet x ) ; :: thesis: A is maximal_anti-discrete

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

( 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
ex x being Point of Y st
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;( 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

( x in A & A = MaxADSet x ) ; :: thesis: A is maximal_anti-discrete

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