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