proposition: Lemma compact_P5 : forall X:R -> Prop, closed_set X -> bounded X -> compact X.
proof: Proof. intros; unfold bounded in H0. elim H0; clear H0; intros m H0. elim H0; clear H0; intros M H0. assert (H1 := compact_P3 m M). apply (compact_P4 (fun c:R => m <= c <= M) X H1 H H0). Qed.
imports: Rbase Rfunctions Ranalysis1 RList List Classical_Prop Classical_Pred_Type