:: deftheorem Def12 defines MSFixPoints CLOSURE1:def 12 :
for I being set
for M being ManySortedSet of I
for F being ManySortedFunction of M,M
for b₄ being ManySortedSubset of M holds
( b₄ = MSFixPoints F iff for x being set
for i being object st i in I holds
( x in b₄ . i iff ex f being Function st
( f = F . i & x in dom f & f . x = x ) ) );