proposition: Lemma inc_parts_containing : forall (a : E) (r : E2P) (y z : E), inc y z -> is_part a r z -> inc z (parts_containing a r y).
proof: Proof. ir. unfold parts_containing in |- *. ap Z_inc. ap powerset_inc. unfold is_part in H0; xd. xd. Qed.
imports: set_theory