:: deftheorem Def2 defines [*] LATSUM_1:def 2 :
for R, S being RelStr
for b₃ being strict RelStr holds
( b₃ = 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 InternalRel of R * the InternalRel of S) ) );