+ apply (prove (A ∨ ¬ A));
+
+ apply (RAA [H] ⊥);
+ apply (¬_e (¬A) A);
+ [ apply (¬_i [H1] ⊥);
+ apply (¬_e (¬(A∨¬A)) (A∨¬A));
+ [ apply [H];
+ | apply (∨_i_l A);
+ apply [H1];
+ ]
+ | apply (RAA [H2] ⊥);
+ apply (¬_e (¬(A∨¬A)) (A∨¬A));
+ [ apply [H];
+ | apply (∨_i_r (¬A));
+ apply [H2];
+ ]
+ ]
+qed.
+
+lemma RA_to_EM1 : A ∨ ¬ A.
+
+ apply (prove (A ∨ ¬ A));
+
+ apply (RAA [H] ⊥);
+ apply (¬_e (¬¬A) (¬A));
+ [ apply (¬_i [H2] ⊥);
+ apply (¬_e (¬(A∨¬A)) (A∨¬A));
+ [ apply [H];
+ | apply (∨_i_r (¬A));
+ apply [H2];
+ ]
+ | apply (¬_i [H1] ⊥);
+ apply (¬_e (¬(A∨¬A)) (A∨¬A));
+ [ apply [H];
+ | apply (∨_i_l A);
+ apply [H1];
+ ]
+ ]
+qed.