for x, y being Nat st x > 1 & y > 1 holds
x * y >= x + y