theorem Th2: :: LEXBFS:2

for n, m, k being Nat st m <= k & n < m holds
k -' m < k -' n