theorem Th2: :: LATSUM_1:2

for R, S being RelStr holds
( the InternalRel of R c= the InternalRel of (R [*] S) & the InternalRel of S c= the InternalRel of (R [*] S) )