for a being Real
for l being Integer st a >= 0 holds
a #Z l >= 0 by Lm5;