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

is mentioned by

Thm*  x:{2...}. prime(x)  (i,j:{2..x}. x = ij & prime(i))	[composite_with_prime_factor]
Thm*  x:. prime(x)  x<2  (i,j:{2..x}. x = ij)	[nonprime_nat]
Thm*  x:. prime(x)  (i:{2..x}. i | x)	[natprime_nondivs]
Thm*  x:. prime(x)  2x & (i:{2..x}. i | x)	[prime_nat]
Thm*  k:, i:{2..k}, j:. ij = k  2  j < k & i<k	[factors_smaller2]

In prior sections: int 1 bool 1 int 2 num thy 1 LogicSupplement

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