theorem Th9: :: LATSUM_1:9

for R, S being non empty RelStr
for a, b being Element of (R [*] S)
for c, d being Element of S st a = c & b = d & R tolerates S & S is transitive holds
( a <= b iff c <= d )