Theorem intersection_idem

Proof
01. ⊢ A ⊆ A, incl_refl.
intersection_idem. ⊢ A ∩ A = A, intersection_from_incl 1.

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