proposition: Lemma Exercise1_15b1 X: sub X (substrate r) -> least_upper_bound (completion_order r) (fun_image X lobs) (uplo_bounds r X).
proof: Proof. move=> Xsr. set Y:= fun_image X _ . have Yc: (sub Y (completion r)). move=> y /funI_P [z zX ->]; apply: Exercise1_15a8. by move=> t /set1_P ->; apply: Xsr. suff: (uplo_bounds r (union Y) = uplo_bounds r X). by move <-; apply: Exercise1_15a14. set_extens t; move /Zo_P => [tsr [_ tp]]; apply: Zo_i => //; split => //; move=> y /Zo_P [ysr [_ uy]]; apply: tp; apply: Zo_i => //; split => // u. move /setU_P => [v vy] /funI_P [z zX vp]. move: vy; rewrite vp => /Zo_P [usr [_ aux]]. move: (aux _ (set1_1 z)) (uy _ zX) => le1 le2; order_tac. move => ux;apply: uy; apply: (@setU_i _ (lo_bounds r (singleton u))). apply: (Exercise1_15a18a (Xsr _ ux)). apply /funI_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)