proposition: Lemma intersecting_classes_eq : forall (a : E) (r : E2P) (x y : E), is_class a r x -> is_class a r y -> nonempty (intersection2 x y) -> x = y.
proof: Proof. ir. pose (class_eq_class_of H). pose (class_eq_class_of H0). nin H1. pose (intersection2_first H1). pose (intersection2_second H1). pose (e _ i). pose (e0 _ i0). rewrite <- e1. rewrite <- e2. tv. Qed.
imports: set_theory