for n, n1, n2 being Nat st ( n1 > n or n2 > n ) holds
n1 + n2 > n