proposition: Lemma class_of_class : forall (a : E) (r : E2P) (y : E), inc y a -> is_class a r (class_of a r y).
proof: Proof. ir. unfold is_class in |- *; xd; ir. ap class_of_part. am. apply nonempty_intro with y. unfold class_of in |- *. ap intersection_inc. apply nonempty_intro with a. unfold parts_containing in |- *; ap Z_inc; xd. ap powerset_inc; unfold sub in |- *; ir; au. ap lem1. ir. unfold parts_containing in H0. zpr H0. xd. unfold class_of in |- *. ap intersection_sub. unfold parts_containing in |- *. ap Z_inc. ap powerset_inc. unfold is_part in H0. xd. xd. nin H1. pose (intersection2_first H1). pose (intersection2_second H1). ap excluded_middle; unfold not in |- *; ir. pose (Z (class_of a r y) (fun v : E => inc v z -> False)). assert (is_part a r e). unfold is_part in |- *. xd. apply sub_trans with (class_of a r y). unfold e in |- *; ap Z_sub. unfold sub in |- *; ir. unfold class_of in H3. apply intersection_forall with (parts_containing a r y). am. unfold parts_containing in |- *. ap Z_inc. ap powerset_inc; unfold sub in |- *; ir; au. xd; try ap lem1; au. ir. unfold e in |- *; Ztac. unfold class_of in |- *. ap intersection_inc; ir. apply nonempty_intro with a. unfold parts_containing in |- *; Ztac; xd. ap powerset_inc; unfold sub in |- *; ir; au. ap lem1. unfold parts_containing in H6. zpr H6. xd. assert (inc x (class_of a r y)). assert (sub e (class_of a r y)). unfold e in |- *; ap Z_sub. ap H9. am. unfold class_of in H9. assert (inc x y1). apply intersection_forall with (parts_containing a r y). am. unfold parts_containing in |- *; ap Z_inc. ap powerset_inc. unfold is_part in H7; xd; au. xd. unfold is_part in H7; xd. apply H11 with x; am. ir. assert (inc x z). unfold is_part in H0; xd. apply H8 with z0; au. assert (sub e a). apply sub_trans with (class_of a r y). unfold e in |- *; ap Z_sub. ap class_of_sub. am. ap lem1. ap H9; am. unfold e in H3. zpr H3. ap H8; am. ir. unfold e in |- *; ap Z_inc. assert (sub e (class_of a r y)). unfold e in |- *; ap Z_sub. ap H6. unfold e in |- *; ap Z_inc. assert (is_part a r (class_of a r y)). ap class_of_part. am. unfold is_part in H7. xd. apply H9 with x. ap H6. am. am. am. ir. assert (inc x z). unfold is_part in H0; xd. apply H8 with z0. am. am. assert (sub e a). apply sub_trans with (class_of a r y). unfold e in |- *; ap Z_sub. ap class_of_sub. am. ap lem1. ap H10; am. unfold e in H3. zpr H3. ap H9; am. ir. assert (inc x z). unfold is_part in H0; xd. apply H7 with z0; au. assert (sub e a). apply sub_trans with (class_of a r y). unfold e in |- *; ap Z_sub. ap class_of_sub. am. ap lem1. ap H9; au. unfold e in H3. zpr H3. ap H8; au. assert (sub (class_of a r y) e). ap class_of_sub. unfold e in |- *; ap Z_inc. ap class_of_origin; au. am. am. assert (inc y0 e). ap H4. am. unfold e in H5. zpr H5. ap H6; au. Qed.
imports: set_theory