proposition: Lemma class_of_origin : forall (a : E) (r : E2P) (y : E), inc y a -> inc y (class_of a r y).
proof: Proof. ir. unfold class_of in |- *. ap intersection_inc. apply nonempty_intro with a. ap inc_parts_containing. am. ap lem1. ir. unfold parts_containing in H0. cp (Z_pr H0). cbv beta in H1. xd; au. Qed.
imports: set_theory