for n, m being Nat st n <> 0 & m <> 0 holds
(((n * m) - n) - m) + 1 >= 0