proposition: Lemma inc_class_of : forall (a : E) (r : E2P) (x y : E), inc x a -> inc y a -> r x y -> inc x (class_of a r y).
proof: Proof. ir. assert (is_part a r (class_of a r y)). ap class_of_part. am. unfold is_part in H2. xd. set (x_ := class_of_origin). apply H4 with y; au. Qed.
imports: set_theory