```
(def-constant br%reflexive
"lambda(r:sets[ind_1,ind_1],
forall(x:ind_1, #(r(x,x))))"
(theory generic-theory-1))
```

```
(def-constant br%symmetric
"lambda(r:sets[ind_1,ind_1],
forall(x,y:ind_1, #(r(x,y)) implies #(r(y,x))))"
(theory generic-theory-1))
```

```
(def-constant br%transitive
"lambda(r:sets[ind_1,ind_1],
forall(x,y,z:ind_1, #(r(x,y)) and #(r(y,z)) implies #(r(x,z))))"
(theory generic-theory-1))
```

```
(def-constant br%equiv%relation
"lambda(r:sets[ind_1,ind_1],
br%reflexive(r) and br%symmetric(r) and br%transitive(r))"
(theory generic-theory-1))
```

```
(def-constant pred%to%rel
"lambda(p:[ind_1,ind_1 -> prop],
lambda(x,y:ind_1, if(p(x,y), an%individual, ?unit%sort)))"
(theory generic-theory-1))

```

```
(def-constant equiv%predicate
"lambda(pred:[ind_1,ind_1 -> prop], br%equiv%relation(pred%to%rel(pred)))"
(theory generic-theory-1))
```

```
(def-theorem characterization-of-equivalence-predicates
"forall(rel:[ind_1,ind_1 -> prop],
equiv%predicate(rel) iff
(forall(a,b,c:ind_1, rel(a,b) and rel(b,c) implies rel(a,c))
and
forall(a:ind_1, rel(a,a))
and
forall(a,b:ind_1, rel(a,b) implies rel(b,a))))"
(theory generic-theory-1)
(proof
(
(unfold-single-defined-constant-globally equiv%predicate)
unfold-defined-constants
unfold-defined-constants
(prove-by-logic-and-simplification 0)
)))
```