theorem Th7: :: EXCHSORT:7

for a, b being Ordinal st not a \ b is empty & a \ b is finite holds
ex n being Nat st a = b +^ n