proposition: Lemma T1graph_p1 a b: (a <= b)%ca -> inc (J (Ro a) (Ro b)) T1graph.
proof: Proof. move => lab. apply/setI2_P; split. by apply/(T1graph_o1 (R_inc a) (R_inc b)); rewrite !B_back. by apply: setXp_i; apply: R_inc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)