theorem :: NAT_3:22

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