Theorem diff_is_involution

Theorem. diff_is_involution
A ⊆ X → X \ (X \ A) = A
Proof
01. 1 ⊢ A ⊆ X, hypo.
02. 2 ⊢ x ∈ X \ (X \ A), hypo.
03. 2 ⊢ x ∈ X, diff_eliml 2.
04. 2 ⊢ ¬x ∈ X \ A, diff_elimr 2.
05. 5 ⊢ ¬x ∈ A, hypo.
06. 2, 5 ⊢ x ∈ X \ A, diff_intro 3 5.
07. 2, 5 ⊢ ⊥, neg_elim 4 6.
08. 2 ⊢ ¬¬x ∈ A, neg_intro 7.
09. 2 ⊢ x ∈ A, dne 8.
10. ⊢ x ∈ X \ (X \ A) → x ∈ A, subj_intro 9.
11. 11 ⊢ x ∈ A, hypo.
12. 1, 11 ⊢ x ∈ X, incl_elim 1 11.
13. 13 ⊢ x ∈ X \ A, hypo.
14. 13 ⊢ ¬x ∈ A, diff_elimr 13.
15. 11, 13 ⊢ ⊥, neg_elim 14 11.
16. 11 ⊢ ¬x ∈ X \ A, neg_intro 15.
17. 1, 11 ⊢ x ∈ X \ (X \ A), diff_intro 12 16.
18. 1 ⊢ x ∈ A → x ∈ X \ (X \ A), subj_intro 17.
19. 1 ⊢ x ∈ X \ (X \ A) ↔ x ∈ A, bij_intro 10 18.
20. 1 ⊢ ∀x. x ∈ X \ (X \ A) ↔ x ∈ A, uq_intro 19.
21. 1 ⊢ X \ (X \ A) = A, ext 20.
diff_is_involution. ⊢ A ⊆ X → X \ (X \ A) = A,
  subj_intro 21.

Dependencies
The given proof depends on six axioms:
comp, efq, eq_refl, eq_subst, ext, lem.