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. * 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: Coq(Classical Description FunctionalExtensionality ProofIrrelevance) ZornsLemma(Classical_Wf EnsemblesSpec Relation_Definitions_Implicit ZornsLemma)