proposition: Lemma setIrel_P z: nonempty z -> forall x y, (related (intersection z) x y <-> (forall r, inc r z -> related r x y)).
proof: Proof. move=> nez x y; apply/(setI_P nez). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)