scheme :: UNIROOTS:sch 1
CompIndNE{ P1[ non zero Nat] } :
for k being non zero Element of NAT holds P1[k]
provided
A1: for k being non zero Element of NAT st ( for n being non zero Element of NAT st n < k holds
P1[n] ) holds
P1[k]