proposition: Lemma dd_pr1 F x y: inc x F -> inc y F -> x <> y -> cardinal (x \cap y) <c (disjointness_degree F).
proof: Proof. move => xF yF xy; apply: csup_s1. move=> t /funI_P [z _ ->]; fprops. apply /funI_P; exists (J x y); last by aw. by apply /setC_P;split; [apply :setXp_i | case /diagonal_pi_P]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)