theorem :: LATSUM_1:23

for R, S being RelStr
for a, b being Element of (R [*] S) st the carrier of R /\ the carrier of S is lower Subset of S & a <= b & b in the carrier of R holds
a in the carrier of R