proposition: Lemma class_of_part : forall (a : E) (r : E2P) (y : E), inc y a -> is_part a r (class_of a r y).
proof: Proof. ir. unfold is_part in |- *; xd; ir. unfold class_of in |- *. ap intersection_sub. unfold parts_containing in |- *. ap Z_inc. ap powerset_inc. unfold sub in |- *; ir; au. xd. ap lem1. unfold class_of in |- *. ap intersection_inc. apply nonempty_intro with a. unfold parts_containing in |- *. ap Z_inc. ap powerset_inc; unfold sub in |- *; ir; au. xd. ap lem1. ir. assert (is_part a r y0). unfold parts_containing in H3. cp (Z_pr H3). cbv beta in H4. xd. unfold is_part in H4; xd. apply H5 with x. apply intersection_forall with (parts_containing a r y). exact H0. am. am. am. unfold class_of in |- *. ap intersection_inc. apply nonempty_intro with a. unfold parts_containing in |- *. ap Z_inc. ap powerset_inc; unfold sub in |- *; ir; au. xd. ap lem1. ir. assert (is_part a r y0). unfold parts_containing in H3. cp (Z_pr H3). cbv beta in H4. xd. unfold is_part in H4; xd. apply H6 with x. apply intersection_forall with (parts_containing a r y). exact H0. am. am. am. Qed.
imports: set_theory