proposition: Lemma class_eq_class_of : forall (a : E) (r : E2P) (y : E), is_class a r y -> forall x : E, inc x y -> class_of a r x = y.
proof: Proof. ir. ap extensionality. ap class_of_sub; au. unfold is_class in H; xd; au. unfold is_class in H. xd. ap H2. ap class_of_part. unfold is_part in H; xd. apply nonempty_intro with x. ap intersection2_inc; au. ap class_of_origin. unfold is_part in H; xd. Qed.
imports: set_theory