for S, T being non empty up-complete Poset
for x being Element of [:S,T:] st x `1 is compact & x `2 is compact holds
x is compact