:: deftheorem defines PartUnion PCOMPS_2:def 1 :
for FX being set
for R being Relation
for B being Element of FX holds PartUnion (B,R) = union (R -Seg B);