proposition: Lemma Exercise4_7i x: sub x (substrate r) -> has_supremum r x.
proof: Proof. move: Exercise4_7b => or xr; case: (emptyset_dichot x) => nex. move: (the_least_pr or Exercise4_7c) => tlp. rewrite nex; exists (the_least r). rewrite lub_set0 //. apply: (lattice_finite_sup2 lr (sub_finite_set xr fs) nex xr). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)