Theorem diff_union

Proof
01. ⊢ A \ B = A ∩ compl B, diff_as_inter.
02. ⊢ (A \ B) ∪ B = (A ∩ compl B) ∪ B, f_equal 1, f x = x ∪ B.
03. ⊢ (A ∩ compl B) ∪ B = (A ∪ B) ∩ (compl B ∪ B), union_distr.
04. ⊢ B ∪ compl B = UnivCl, union_compl.
05. ⊢ compl B ∪ B = B ∪ compl B, union_comm.
06. ⊢ compl B ∪ B = UnivCl, eq_trans 5 4.
07. ⊢ (A ∪ B) ∩ (compl B ∪ B) = (A ∪ B) ∩ UnivCl,
  f_equal 6, f x = (A ∪ B) ∩ x.
08. ⊢ (A ∪ B) ∩ UnivCl = A ∪ B, intersection_neutr.
09. ⊢ (A ∪ B) ∩ (compl B ∪ B) = A ∪ B, eq_trans 7 8.
10. ⊢ (A ∩ compl B) ∪ B = A ∪ B, eq_trans 3 9.
diff_union. ⊢ (A \ B) ∪ B = A ∪ B, eq_trans 2 10.

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