:: deftheorem Def10 defines a_partition PUA2MSS1:def 10 :
for A being partial non-empty UAStr
for b₂ being a_partition of the carrier of A holds
( b₂ is a_partition of A iff for f being operation of A holds f is_exactly_partitable_wrt b₂ );