DiscreteMath Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
4Thm*  a:b:. {a...b} ~ {a..(b+1)}[intiseg_intseg_plus]
cites the following:
3Thm*  a,b',b:b = b'+1  ({a...b'} ~ {a..b})[intiseg_intseg]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
DiscreteMath Sections DiscrMathExt Doc