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