proposition: Lemma criterion : forall p : EP, ex (fun x : E => forall y : E, p y -> inc y x) -> axioms p.
proof: Proof. ir. nin H. unfold axioms in |- *. eapply ex_intro with (Z x p). unfold property in |- *. ir; xd; ir. ap Z_inc. ap H; au. au. apply Z_pr with x. am. Qed.
imports: set_theory