let S, T be non empty up-complete Poset; :: thesis: for x being Element of [:S,T:] st x `1 is compact & x `2 is compact holds
x is compact
let x be Element of [:S,T:]; :: thesis: ( x `1 is compact & x `2 is compact implies x is compact )
assume ( x `1 << x `1 & x `2 << x `2 ) ; :: according to WAYBEL_3:def 2 :: thesis: x is compact
hence x << x by Th21; :: according to WAYBEL_3:def 2 :: thesis: verum