theorem Th21: :: NAT_3:21

for n being Nat st n <> 1 holds
n |-count 1 = 0