(defrelation binrel (?r ?s) := (and (binary-relation ?r) (subset (universe ?r) ?s)))
(defrelation reflexive (?r ?s) := (and (binrel ?r ?s) (forall ?x (=> (member ?x ?s) (holds ?r ?x ?x)))))
(defrelation irreflexive (?r ?s) := (and (binrel ?r ?s) (forall (?x) (=> (member ?x ?s) (not (holds ?r ?x ?x))))))
(defrelation symmetric (?r ?s) := (and (binrel ?r ?s) (forall (?x ?y) (=> (holds ?r ?x ?y) (holds ?r ?y ?x)))))
(defrelation asymmetric (?r ?s) := (and (binrel ?r ?s) (forall (?x ?y) (=> (holds ?r ?x ?y)) (not (holds ?r ?y ?x))))))
(defrelation antisymmetric (?r ?s) := (and (binrel ?r ?s) (forall (?x ?y) (=> (holds ?r ?x ?y) (holds ?r ?y ?x) (= ?x ?y)))))
(defrelation trichotomizes (?r ?s) := (and (binrel ?r ?s) (forall (?x ?y) (=> (member ?x ?s) (member ?y ?s) (or (holds ?r ?x ?y) (= ?x ?y) (holds ?r ?y ?x))))))
(defrelation transitive (?r ?s) := (and (binrel ?r ?s) (forall (?x ?y ?z) (=> (holds ?r ?x ?y) (holds ?r ?y ?z) (holds ?r ?x ?z)))))