theorem Th17: :: LATSUM_1:17

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