theorem :: YELLOW_3:18

for X, Y being non empty reflexive RelStr st [:X,Y:] is with_suprema holds
( X is with_suprema & Y is with_suprema )