:: deftheorem DefUnion defines Union ROUGHS_3:def 1 :
for R1, R2 being RelStr
for b₃ being strict RelStr holds
( b₃ = Union (R1,R2) iff ( the carrier of b₃ = the carrier of R1 \/ the carrier of R2 & the InternalRel of b₃ = the InternalRel of R1 \/ the InternalRel of R2 ) );