theorem :: NAT_3:57

for n being non zero Nat st support (ppf n) = {} holds
n = 1