:: deftheorem defines DisjointFam PCOMPS_2:def 2 :
for FX being set
for R being Relation
for b₃ being set holds
( b₃ = DisjointFam (FX,R) iff for A being set holds
( A in b₃ iff ex B being Element of FX st
( B in FX & A = B \ (PartUnion (B,R)) ) ) );