proposition: Lemma saturated_setI r x: equivalence r -> nonempty x -> (alls x (sub^~ (substrate r))) -> (alls x (saturated r)) -> (sub (intersection x) (substrate r) /\ saturated r (intersection x)).
proof: Proof. move=> er nex als alsa. have aux: (sub (intersection x) (substrate r)). by move: nex => [y yx]; apply: sub_trans (als _ yx); apply: setI_s1. split =>//; apply /(saturatedP er aux) => y yi t tc; apply: (setI_i nex). move=> z zx; move:(alsa _ zx). move /(saturatedP er (als _ zx))=> s; apply: (s _ (setI_hi yi zx) _ tc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)