proposition: Lemma included3_compact : forall x y z Hxyz, Compact Hab x -> Compact Hab y -> Compact Hab z -> included (compact (Min (Min x y) z) (Max (Max x y) z) Hxyz) (Compact Hab).
proof: Proof. do 4 intro. intros H H0 H1. inversion_clear H. inversion_clear H0. inversion_clear H1. apply included_compact; split. repeat apply leEq_Min; auto. apply leEq_transitive with z. apply Min_leEq_rht. auto. apply leEq_transitive with z. auto. apply rht_leEq_Max. repeat apply Max_leEq; auto. Qed.
imports: CoRN.algebra.CSetoidInc CoRN.reals.RealLists