theorem Th18: :: LATSUM_1:18

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