Definition chain_lub' {P : Poset} (P_CC : is_chain_complete P) {I:UU} (p:I->P) : is_chain p -> least_upper_bound p. Proof. intros p_chain. exact (chain_lub P_CC (I,,(p,,p_chain))). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.OrderTheory.OrderedSets.WellOrderedSets. Require Import UniMath.OrderTheory.DCPOs.AlternativeDefinitions.Dcpo. Require Import UniMath.OrderTheory.Posets.Subposets.