scheme :: NAT_4:sch 4
scheme4{ F1( set , set ) -> set , P1[ set , set ] } :
for n, m being Element of NAT
for r being Real
for X being finite set st X = { F1(p,m) where p is prime Element of NAT : ( p <= r & P1[p,m] ) } & r >= 0 holds
card X <= [\r/]