rel 1 Sections StandardLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def strict_part(x,y.R(x;y);a;b) == R(a;b) & R(b;a)

is mentioned by

Thm* R:(TTProp). 
Thm* (x,y:T. Dec(R(x,y)))
Thm* 
Thm* Linorder(T;x,y.R(x,y))  (a,b:T. strict_part(x,y.R(x,y);a;b)  R(b,a))		[linorder_lt_neg]
Thm* R:(TTProp). 
Thm* Linorder(T;x,y.R(x,y))  (a,b:T. R(a,b)  strict_part(x,y.R(x,y);b;a))		[linorder_le_neg]
Thm* R:(TTProp). 
Thm* (Trans a,b:T. R(a,b))
Thm* 
Thm* (a,b,c:T.
Thm* (strict_part(x,y.R(x,y);a;b)  R(b,c)  strict_part(x,y.R(x,y);a;c))		[trans_imp_sp_trans_b]
Thm* R:(TTProp). 
Thm* (Trans a,b:T. R(a,b))
Thm* 
Thm* (a,b,c:T.
Thm* (R(a,b)  strict_part(x,y.R(x,y);b;c)  strict_part(x,y.R(x,y);a;c))		[trans_imp_sp_trans_a]
Thm* R:(TTProp). 
Thm* (Trans a,b:T. R(a,b))  (Trans a,b:T. strict_part(x,y.R(x,y);a;b))		[trans_imp_sp_trans]
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:(TTProp). 
Thm* (a,b:T. Dec(R(a,b)))
Thm* 
Thm* (Connex(T;x,y.R(x,y))
Thm* (
Thm* ((a,b:T.
Thm* ((strict_part(x,y.R(x,y);a;b)
Thm* (( Symmetrize(x,y.R(x,y);a;b)
Thm* (( strict_part(x,y.R(x,y);b;a)))		[connex_iff_trichot]
Thm* R:(TTProp), a,b:T. strict_part(x,y.R(x,y);a;b)  a = b[strict_part_irrefl]

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

rel 1 Sections StandardLIB Doc