theorem Th53: :: YELLOW10:53

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 (compactbelow x) = compactbelow (x `2)