proposition: Theorem part_set_is_strictly_greater_than_set1 : False.
proof: Proof. case invX. intros x H'; try assumption. cut (~ in_part x X). intros H'0; try assumption. absurd (in_part x X); auto with algebra. simpl in |- *. unfold X_def in |- *. apply not_inpart_comp_r with X; auto with algebra. unfold not in |- *. intros H'0; try assumption. absurd (in_part x X); auto with algebra. apply not_inpart_comp_r with (Ap f x); auto with algebra. Qed.
imports: Sets