Def  i  j < k == (ij)(j<k)

is mentioned by

Thm*  i,j,k:. i  j < k  i  j < k	[lelt_int_vs_lelt]
Def  complete_intseg_mset(a; b; f)(x) == if a  x < b f(x) else 0 fi	[complete_intseg_mset]

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