rel 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def Order(T;x,y.R(x;y))
Def == Refl(T;x,y.R(x;y)) & (Trans x,y:T. R(x;y)) & AntiSym(T;x,y.R(x;y))

is mentioned by

Thm* R:(TTProp). 
Thm* Order(T;x,y.R(x,y))
Thm* 
Thm* (x,y:T. Dec(x = y))
Thm* 
Thm* (a,b:T. R(a,b)  strict_part(x,y.R(x,y);a;b)  a = b)		[order_split]
Thm* R,R':(TTProp).
Thm* (x,y:T. R(x,y)  R'(x,y))
Thm* 
Thm* (Order(T;x,y.R(x,y))  Order(T;x,y.R'(x,y)))		[order_functionality_wrt_iff]
Def Linorder(T;x,y.R(x;y)) == Order(T;x,y.R(x;y)) & Connex(T;x,y.R(x;y))[linorder]

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

rel 1 Sections StandardLIB Doc