proposition: Lemma setIrelT z: (alls z transitivep) -> transitivep (intersection z).
proof: Proof. move=> allt; case: (emptyset_dichot z). move => ->; rewrite setI_0 => a b c;case; case. move=> neX y x u /(setIrel_P neX) rxy /(setIrel_P neX) ryz. apply/(setIrel_P neX) => r rz. exact: ((allt _ rz) _ _ _ (rxy _ rz) (ryz _ rz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)