proposition: Lemma chains_sup_correct (F : Ensemble chains) (P : chain chains_ord F) : let U := chains_sup_def F P in (forall S:chains, In F S -> chains_ord S U) /\ (forall T:chains, (forall S:chains, In F S -> chains_ord S T) -> chains_ord U T).
proof: Proof. intros. unfold chains_ord, Included, U. split; intros. - constructor. now exists S. - destruct H0 as [[x0 [? H1]]]. now apply H in H1. Qed.
imports: Classical ClassicalChoice Relation_Definitions Relation_Definitions_Implicit Ensembles EnsemblesImplicit ProofIrrelevance InverseImage EnsemblesSpec Quotients EnsemblesSpec