proposition: Lemma trans_criterion : forall (p : EP) (f : E1) (x : E), (forall y : E, p y -> ex (fun z : E => A (inc z x) (f z = y))) -> axioms p.
proof: Proof. ir. ap criterion. sh (Image.create x f). ir. ap Image.show_inc. ap H. am. Qed.
imports: set_theory