theorem Th45: :: YELLOW10:45

for S, T being non empty reflexive antisymmetric up-complete RelStr
for x being Element of [:S,T:] holds
( proj1 (waybelow x) c= waybelow (x `1) & proj2 (waybelow x) c= waybelow (x `2) )