proposition: Lemma related_classes_eq : forall (a : E) (r : E2P) (x y : E), inc x a -> inc y a -> r x y -> class_of a r x = class_of a r y.
proof: Proof. ir. ap intersecting_classes_of_eq; au. apply nonempty_intro with x. pose class_of_origin. pose inc_class_of. ap intersection2_inc; au. Qed.
imports: set_theory