:: deftheorem Def11 defines IndexedPartition PUA2MSS1:def 11 :
for A being partial non-empty UAStr
for b₂ being IndexedPartition of the carrier of A holds
( b₂ is IndexedPartition of A iff rng b₂ is a_partition of A );