theorem Cantor5: :: NUMBER12:38
for f being natural-valued increasing Arithmetic_Progression st ( for i being Nat st i < 10 holds
f . i is odd Prime ) holds
difference f >= 210 by NAT_D:7, Cantor5Div;