proposition: Lemma partial_WO_chain_ub_correct: forall (C:Ensemble partial_WO) (c:chain partial_WO_ord C), forall WO:partial_WO, In C WO -> partial_WO_ord WO (partial_WO_chain_ub C c).
proof: Proof. intros. constructor. unfold Included. intros. constructor. exists WO. tauto. intros. split. intro. exists WO. tauto. intro. destruct H2. destruct H2. case (c WO x0 H H2). intro. destruct H4. apply <- pwo_restriction0. assumption. assumption. assumption. intro. destruct H4. apply -> pwo_restriction0. assumption. pose proof (pwo_R_lives_on_S x0 x y). tauto. pose proof (pwo_R_lives_on_S x0 x y). tauto. intros. destruct H2. destruct H2. case (c WO x0 H H2). intro. destruct H4. apply pwo_downward_closed0 with y. assumption. pose proof (pwo_R_lives_on_S x0 x y). tauto. assumption. intro. apply H4. pose proof (pwo_R_lives_on_S x0 x y). tauto. Qed.
imports: Relation_Definitions Relation_Definitions_Implicit Classical_Wf Description FunctionalExtensionality Classical ZornsLemma ProofIrrelevance EnsemblesSpec