theorem :: NAT_2:19

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