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