- some additions and corrections

[helm.git] / matita / matita / lib / basics / relations.ma

diff --git a/matita/matita/lib/basics/relations.ma b/matita/matita/lib/basics/relations.ma
index d74380de43938650d6de559ba8e3e67384251f70..f469ddca29f72fe1eeaeea9d50752fefed34aad2 100644 (file)
--- a/matita/matita/lib/basics/relations.ma
+++ b/matita/matita/lib/basics/relations.ma
@@ -167,6 +167,9 @@ definition bi_relation: Type[0] → Type[0] → Type[0]
 definition bi_reflexive: ∀A,B. ∀R:bi_relation A B. Prop
 ≝ λA,B,R. ∀x,y. R x y x y.
 
+definition bi_symmetric: ∀A,B. ∀R: bi_relation A B. Prop ≝ λA,B,R.
+                         ∀a1,a2,b1,b2. R a2 b2 a1 b1 → 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.