theorem Th47: :: YELLOW10:47

for S being non empty lower-bounded up-complete Poset
for T being non empty up-complete Poset
for x being Element of [:S,T:] holds proj2 (waybelow x) = waybelow (x `2)