(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)
        )))