Theorem lem_from_dne

Theorem. lem_from_dne
A ∨ ¬A
Proof
01. 1 ⊢ ¬(A ∨ ¬A), hypo.
02. 2 ⊢ A, hypo.
03. 2 ⊢ A ∨ ¬A, disj_introl 2.
04. 1, 2 ⊢ ⊥, neg_elim 1 3.
05. 1 ⊢ ¬A, neg_intro 4.
06. 1 ⊢ A ∨ ¬A, disj_intror 5.
07. 1 ⊢ ⊥, neg_elim 1 6.
08. ⊢ ¬¬(A ∨ ¬A), neg_intro 7.
lem_from_dne. ⊢ A ∨ ¬A, dne 8.

Dependencies
The given proof depends on two axioms:
efq, lem.