-definition tri_RC: ∀A,B,C. tri_relation A B C → tri_relation A B C ≝
- λA,B,C,R,a1,b1,c1,a2,b2,c2. R … a1 b1 c1 a2 b2 c2 ∨
- ∧∧ a1 = a2 & b1 = b2 & c1 = c2.
+definition tri_RC (A,B,C): tri_relation A B C → tri_relation A B C ≝
+ λR,a1,b1,c1,a2,b2,c2.
+ ∨∨ R … a1 b1 c1 a2 b2 c2
+ | ∧∧ a1 = a2 & b1 = b2 & c1 = c2.