for I being set
for A, M being ManySortedSet of I
for F being ManySortedFunction of M,M holds
( ( A in M & F .. A = A ) iff A in MSFixPoints F )