:: deftheorem Def36 defines pcs-union PCS_0:def 36 :
for I being set
for C being () ManySortedSet of I
for b₃ being strict pcs-Str holds
( b₃ = pcs-union C iff ( the carrier of b₃ = Union (Carrier C) & the InternalRel of b₃ = Union (pcs-InternalRels C) & the ToleranceRel of b₃ = Union (pcs-ToleranceRels C) ) );