. x ~ y;x,y.x | y)
R:(T
TProp).
Thm* Preorder(T;x,y.R(x,y))
(EquivRel a,b:T. Symmetrize(x,y.R(x,y);a;b))| Rank | Theorem | Name |
| 2 | . x ~ y | [assoced_equiv_rel] |
| cites the following: | ||
| 1 | ;x,y.x | y) | [divides_preorder] |
| 0 | R:(TTProp).
Thm* Preorder(T;x,y.R(x,y)) (EquivRel a,b:T. Symmetrize(x,y.R(x,y);a;b)) | [symmetrized_preorder] |