proposition: Lemma AS8 : AS8_def.
proof: Proof. move => R hyp Y. pose p y := (fun X => forall x : Set, R x y -> inc x X). pose XX y := choose (p y). have h x y : R x y -> inc x (XX y). move => rxy; move: (hyp y) => ee; exact: (choose_pr ee x rxy). exists (Zo (unionf Y XX) (fun x => (exists2 y, inc y Y & R x y))) => t; split. by move/Zo_hi. move => hx; apply: Zo_i => //. by move: hx => [y ya yb]; apply/setUf_P; exists y => //; apply: h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)