proposition: Lemma setIt_hi (I:Set) (f:I-> Set) x j: inc x (intersectiont f) -> inc x (f j).
proof: Proof. have neJ: nonempty I by exists (Ro j); exists j. move /(setIt_P _ neJ); apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)