Def i  j < k == ij & j<k

is mentioned by

Thm* i,j:, y:{i..j}. i  y < j	[int_seg_properties]
Def {i..j} == {k:| i  k < j }	[int_seg]

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