proposition: Lemma Exercise4_7n a: inc a (substrate r) -> exists S, [/\ finite_set S, nonempty S, sub S (substrate r), (forall x, inc x S -> sup_irred r x) & supremum r S = a].
proof: Proof. move=> asr. have sE: sub (E47S r a) (substrate r) by apply: Zo_S. move: (sub_finite_set sE fs) => fsE. move: (Exercise4_7h asr) (Exercise4_7l asr) => ne ass. by exists (E47S r a);split => // x /Zo_hi []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)