proposition: Lemma related_equivalent : forall (a : E) (r : E2P) (x y : E), inc x a -> inc y a -> r x y -> equivalent a r x y.
proof: Proof. ir. unfold equivalent in |- *; xd. ap intersecting_classes_of_eq; au. apply nonempty_intro with x. ap intersection2_inc. ap class_of_origin; au. ap inc_class_of; au. Qed.
imports: set_theory