union_idem

Theorem. union_idem
A ∪ A = A

Proof
01. ⊢ A ⊆ A, incl_refl.
union_idem. ⊢ A ∪ A = A, union_from_incl 1.

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