proposition: Lemma equivalent_related : forall (a : E) (r : E2P) (x y : E), is_eq_reln a r -> equivalent a r x y -> r x y.
proof: Proof. ir. unfold is_eq_reln in H; xd. set (z := Z a (fun u : E => r x u)). assert (inc y z). unfold equivalent in H0; xd. assert (sub (class_of a r y) z). rewrite <- H4. ap class_of_sub. unfold z in |- *; Ztac. unfold is_part in |- *; xd. unfold z in |- *; ap Z_sub. ir. unfold z in |- *; Ztac. apply H2 with x0. am. assert (sub z a); [ unfold z in |- *; ap Z_sub | ap H8; au ]. au. unfold z in H5; Ztac. am. ir. unfold z in |- *; Ztac. apply H2 with x0; au. assert (sub z a); [ unfold z in |- *; ap Z_sub | ap H8; au ]. unfold z in H5; Ztac. ap H1; au. assert (sub z a); [ unfold z in |- *; ap Z_sub | ap H8; au ]. ap H5. ap class_of_origin. am. unfold z in H3; Ztac. Qed.
imports: set_theory