let n, m be Nat; :: thesis: ( n <> 0 & m <> 0 implies (((n * m) - n) - m) + 1 >= 0 )
assume that
A1: n <> 0 and
A2: m <> 0 ; :: thesis: (((n * m) - n) - m) + 1 >= 0
m >= 0 + 1 by A2, NAT_1:13;
then A3: m - 1 >= (0 + 1) - 1 ;
n >= 0 + 1 by A1, NAT_1:13;
then n - 1 >= (0 + 1) - 1 ;
then (n - 1) * (m - 1) >= 0 by A3;
hence (((n * m) - n) - m) + 1 >= 0 ; :: thesis: verum