Def {i..j} == {k:| i  k < j }

is mentioned by

Thm* P:(Prop). (i:. (j:i. P(j))  P(i))  (i:. P(i))	[complete_nat_ind_with_y]
Thm* P:(Prop). (i:. (j:i. P(j))  P(i))  (i:. P(i))	[complete_nat_ind]
Thm* i,j:, x,y:{i..j}. Dec(x = y)	[decidable__equal_int_seg]
Thm* i,j:, y:{i..j}. i  y < j	[int_seg_properties]

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