proposition: Lemma setIt_s2 (I:Set) (f: I-> Set) x: nonempty I -> (forall i, sub x (f i)) -> sub x (intersectiont f).
proof: Proof. by move=> ne hyp t tx; apply/setIt_P => // j; apply: hyp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)