proposition: Lemma Ex4_11_minR_mb R: (forall x, inc x R -> finite_set x) -> mobile_r R -> mobile_r (min_incl_r R).
proof: Proof. move => h mb. move => x y /Zo_P [xR _] /Zo_P [yR _] xy z zi. move: (mb _ _ xR yR xy _ zi) => [Z [za zb zc]]. move: (Ex4_11_minR_pr h za) => [T ta tb]. exists T; split => //; [ by apply: (sub_trans ta zb) | fprops ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)