:: deftheorem Def3 defines sum_of NECKLA_2:def 3 :
for R, S being RelStr
for b₃ being strict RelStr holds
( b₃ = sum_of (R,S) iff ( the carrier of b₃ = the carrier of R \/ the carrier of S & the InternalRel of b₃ = (( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:] ) );