a,b:
. {a...b} ~ 
(1+b-a)a:, b:. {a...b} ~ {a..(b+1)
}a,b:. {a..b} ~ (b-a)| Rank | Theorem | Name |
| 5 | a,b:. {a...b} ~ (1+b-a) | [nsub_intiseg_rw] |
| cites the following: | ||
| 4 | a:, b:. {a...b} ~ {a..(b+1)} | [intiseg_intseg_plus] |
| 2 | a,b:. {a..b} ~ (b-a) | [nsub_intseg_rw] |