proposition: Lemma Exercise1_5b r x: order r -> inc x (substrate r) -> inc (singleton x) (free_subsets r).
proof: Proof. move=> or xsr; apply: Zo_i; first by apply /setP_P; apply: set1_sub. by move=> u v /set1_P -> /set1_P ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)