is mentioned by

Thm* R:(TTProp).  Thm* Preorder(T;x,y.R(x,y))  (EquivRel a,b:T. Symmetrize(x,y.R(x,y);a;b))

[symmetrized_preorder]

Try larger context: StandardLIB IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html