proposition: Lemma range_inc : forall f z : E, axioms f -> ex (fun y : E => A (inc y (domain f)) (V y f = z)) -> inc z (range f).
proof: Proof. ir. nin H0. xd. unfold range in |- *. ap Image.show_inc. apply ex_intro with (pair x z). xd. ap V_inc. unfold domain in H0. pose (Image.ex H0). nin e; xd. apply ex_intro with (pr2 x0). rewrite <- H3. unfold axioms in H. xd. rewrite H. am. am. au. ap pr2_pair. Qed.
imports: set_theory