proposition: Lemma is_class_in_quotient : forall (a : E) (r : E2P) (x : E), is_class a r x -> inc x (quotient a r).
proof: Proof. ir. unfold quotient in |- *; ap Z_inc. ap powerset_inc. unfold is_class in H. xd. unfold is_part in H; xd; au. am. Qed.
imports: set_theory