for n being non zero Nat st n <> 1 holds
n > 1