theorem Th16: :: HILB10_1:13

for n being Nat
for a being non trivial Nat holds Py (a,n) >= n