theorem Th15: :: EXCHSORT:15

( base- {} = 0 & limit- {} = 0 & len- {} = 0 )