:: deftheorem Def7 defines partition-membered EQREL_1:def 7 :
for X being set
for F being Family-Class of X holds
( F is partition-membered iff for S being set st S in F holds
S is a_partition of X );