Theorem intersection_neutl

Proof
01. ⊢ UnivCl ∩ A = A ∩ UnivCl, intersection_comm.
intersection_neutl. ⊢ UnivCl ∩ A = A, eq_trans 1 intersection_neutr.

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