:: deftheorem Def2 defines union_of NECKLA_2:def 2 :
for R, S being RelStr
for b₃ being strict RelStr holds
( b₃ = union_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 ) );