∀ {α : Type u_1} {β : Type u_2} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  (c : OmegaCompletePartialOrder.Chain (α × β)) (i : ℕ), (c i).1 ≤ (Prod.ωSupImpl c).1 ∧ (c i).2 ≤ (Prod.ωSupImpl c).2