Def  Trans x,y:T. E(x;y) == a,b,c:T. E(a;b)  E(b;c)  E(a;c)

is mentioned by

Thm*  (A:Type, R:(AAProp). Thm*  ((A) & (Trans x,y:A. R(x;y)) & (x:A. y:A. R(x;y)) Thm*  (& (x:A. R(x;x)) Thm*  (& Finite(A))	[no_finite_model]
Thm*  R:(AAProp).  Thm*  (A) & (Trans x,y:A. R(x;y)) & (x:A. y:A. R(x;y)) Thm*   Thm*  (k:. f:(kA). i,j:k. i<j  R(f(i);f(j)))	[no_finite_model_lemma]

In prior sections: rel 1

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