1. a : 
2. b : 
3. c : {a...b}
4. {a..b} ~ ({x:{a..b}| x<c }+{x:{a..b}| x<c })
  ({a..c}+{c..b}) ~ ({x:{a..b}| x<c }+{x:{a..b}| x<c })

By:	BackThru: Thm*  (A ~ A')  (B ~ B')  ((A+B) ~ (A'+B')) THEN OOCifExteq

1	{a..c} =ext {x:{a..b}| x<c }	1 step
2	{c..b} =ext {x:{a..b}| x<c }	1 step

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html