theorem Th10: :: LATSUM_1:10

for R, S being non empty reflexive transitive antisymmetric with_suprema RelStr
for x being set st x in the carrier of R holds
x is Element of (R [*] S)