:: deftheorem Def1 defines bool MBOOLEAN:def 1 :
for I being set
for A, b₃ being ManySortedSet of I holds
( b₃ = bool A iff for i being object st i in I holds
b₃ . i = bool (A . i) );