proposition: Lemma Exercise1_11j r: total_order r -> finite_set (substrate r) -> ne_substrate r -> complete_lattice r.
proof: Proof. move => tor fsr nes. move: (tor) => [or _];apply: Exercise1_11b => // X Xsr. case: (emptyset_dichot X) => xE. move: (finite_set_torder_least tor fsr nes) => [x [xsr xl]]. exists x; apply /lubP => //; split. by split =>//; rewrite xE => y /in_set0. by move => z [ze _]; apply: xl. move: (sub_finite_set Xsr fsr) => fsx. move: (finite_subset_torder_greatest tor fsx xE Xsr) => [x []]. rewrite (iorder_sr or Xsr) => xsr xg; exists x; apply /lubP => //; split. split => //; [ by apply: Xsr | move => y yX ; exact: (iorder_gle1 (xg _ yX))]. by move => z [sr]; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)