definition bi_transitive: ∀A,B. ∀R: bi_relation A B. Prop ≝ λA,B,R.
∀a1,a,b1,b. R a1 b1 a b →
∀a2,b2. R a b a2 b2 → R a1 b1 a2 b2.
definition bi_transitive: ∀A,B. ∀R: bi_relation A B. Prop ≝ λA,B,R.
∀a1,a,b1,b. R a1 b1 a b →
∀a2,b2. R a b a2 b2 → R a1 b1 a2 b2.