proposition: Lemma intersecting_classes_of_eq : forall (a : E) (r : E2P) (x y : E), inc x a -> inc y a -> nonempty (intersection2 (class_of a r x) (class_of a r y)) -> class_of a r x = class_of a r y.
proof: Proof. ir. pose class_of_class. apply intersecting_classes_eq with a r; au. Qed.
imports: set_theory