for S, T being non empty up-complete Poset
for s being Element of S
for t being Element of T holds [:(compactbelow s),(compactbelow t):] = compactbelow [s,t]