{α : Type u_6} →
  [inst : OmegaCompletePartialOrder α] →
    (p : α → Prop) →
      (∀ (c : OmegaCompletePartialOrder.Chain α), (∀ i ∈ c, p i) → p (OmegaCompletePartialOrder.ωSup c)) →
        OmegaCompletePartialOrder (Subtype p)