:: deftheorem Def4 defines a_partition EQREL_1:def 4 :
for X being set
for b₂ being Subset-Family of X holds
( b₂ is a_partition of X iff ( union b₂ = X & ( for A being Subset of X st A in b₂ holds
( A <> {} & ( for B being Subset of X holds
( not B in b₂ or A = B or A misses B ) ) ) ) ) );