diff --git a/Lebesgue/measurable_Rbar.v b/Lebesgue/measurable_Rbar.v
index e3a08747b5df0b55efcbf6a268c97de9a4b44f6a..1603f640bef35d3f81cbb9e4dc4f62be2d2b9909 100644
--- a/Lebesgue/measurable_Rbar.v
+++ b/Lebesgue/measurable_Rbar.v
@@ -167,8 +167,7 @@ unfold measurable_Rbar_R.
 intros A HA; rewrite down_union_seq; apply measurable_union_seq; easy.
 Qed.
 
-Lemma measurable_Rbar_R_is_sigma_algebra :
-  is_Sigma_algebra measurable_Rbar_R.
+Lemma measurable_Rbar_R_is_sigma_algebra : is_Sigma_algebra measurable_Rbar_R.
 Proof.
 apply Sigma_algebra_equiv; repeat split.
 apply measurable_Rbar_R_empty.
@@ -176,43 +175,75 @@ apply measurable_Rbar_R_compl.
 apply measurable_Rbar_R_union_seq.
 Qed.
 
-Lemma measurable_Rbar_R_Borel :
-  Incl measurable_Borel_Rbar measurable_Rbar_R.
+Lemma measurable_Rbar_R_Borel : Incl measurable_Borel_Rbar measurable_Rbar_R.
 Proof.
 apply measurable_gen_lub_alt.
 apply measurable_Rbar_R_is_sigma_algebra.
 apply measurable_Rbar_R_open.
 Qed.
 
-Lemma measurable_Borel_Rbar_R :
-  Incl measurable_Rbar_R measurable_Borel_Rbar.
+Lemma measurable_Borel_Rbar_R_up_id :
+  forall A, measurable_R A -> measurable_Borel_Rbar (up_id A).
 Proof.
-rewrite measurable_Rbar_R_eq; unfold measurable_Borel_Rbar, measurable_Borel.
-intros B HB.
-induction HB as [A HA | A HA | A HA | A HA]; rewrite measurable_R_eq_Borel in HA.
-(* . *)
-induction HA as [A HA | | A HA1 HA2 | A HA1 HA2].
-rewrite <- Rbar_subset_open_correct; apply measurable_gen; apply RbSO_woinf; easy.
-admit. (* rewrite up_id_empty. does not work! R vs R_UniformSpace... *)
+rewrite measurable_R_eq_Borel.
+intros A HA; induction HA as [A HA | | A HA1 HA2 | A HA1 HA2].
+(* *)
+apply measurable_gen; rewrite <- Rbar_subset_open_correct; apply RbSO_woinf; easy.
+(* *)
+apply measurable_ext with emptyset;
+    [rewrite <- up_id_empty at 1; easy | apply measurable_empty].
+(* *)
 rewrite up_id_compl; apply measurable_compl.
-admit.
-
+repeat apply measurable_union; try easy; apply measurable_Borel_Rbar_singleton.
+(* *)
 rewrite up_id_union_seq; apply measurable_union_seq; easy.
+Qed.
 
-admit.
-admit.
-admit.
+Lemma measurable_Borel_Rbar_R_up_m :
+  forall A, measurable_R A -> measurable_Borel_Rbar (up_m A).
+Proof.
+intros; apply measurable_union.
+apply measurable_Borel_Rbar_R_up_id; easy.
+apply measurable_Borel_Rbar_singleton.
+Qed.
 
-Admitted.
+Lemma measurable_Borel_Rbar_R_up_p :
+  forall A, measurable_R A -> measurable_Borel_Rbar (up_p A).
+Proof.
+intros; apply measurable_union.
+apply measurable_Borel_Rbar_R_up_id; easy.
+apply measurable_Borel_Rbar_singleton.
+Qed.
+
+Lemma measurable_Borel_Rbar_R_up_mp :
+  forall A, measurable_R A -> measurable_Borel_Rbar (up_mp A).
+Proof.
+intros; apply measurable_union.
+apply measurable_Borel_Rbar_R_up_m; easy.
+apply measurable_Borel_Rbar_singleton.
+Qed.
 
-Lemma measurable_Rbar_R_correct :
-  measurable_Rbar_R = measurable_Borel_Rbar.
+Lemma measurable_Borel_Rbar_R : Incl measurable_R_Rbar measurable_Borel_Rbar.
+Proof.
+intros B HB; induction HB as [A HA | A HA | A HA | A HA].
+apply measurable_Borel_Rbar_R_up_id; easy.
+apply measurable_Borel_Rbar_R_up_m; easy.
+apply measurable_Borel_Rbar_R_up_p; easy.
+apply measurable_Borel_Rbar_R_up_mp; easy.
+Qed.
+
+Lemma measurable_Rbar_R_correct : measurable_Rbar_R = measurable_Borel_Rbar.
 Proof.
 apply Ext_equiv; split.
-apply measurable_Borel_Rbar_R.
+rewrite measurable_Rbar_R_eq; apply measurable_Borel_Rbar_R.
 apply measurable_Rbar_R_Borel.
 Qed.
 
+Lemma measurable_R_Rbar_correct : measurable_R_Rbar = measurable_Borel_Rbar.
+Proof.
+rewrite <- measurable_Rbar_R_eq; apply measurable_Rbar_R_correct.
+Qed.
+
 End measurable_Rbar_Borel_Facts.