Definition is_chain_complete_subposet {P : Poset} (P_CC : is_chain_complete P) {A : Subposet P} (A_chain_closed : forall C : Chain_hsubtype A, A (chain_lub P_CC (fmap_chain subposet_incl C))) : is_chain_complete A. Proof. intros C. use make_least_upper_bound. { exists (chain_lub P_CC (fmap_chain subposet_incl C)). apply A_chain_closed. } apply is_least_upper_bound_in_subposet. apply least_upper_bound_property. 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.