theorem :: NUMBER06:52

for f being Arithmetic_Progression holds
( not difference f = 1000 or for p1, p2, p3 being Prime
for i being Nat holds
( not p1,p2,p3 are_mutually_distinct or not p1 = f . i or not p2 = f . (i + 1) or not p3 = f . (i + 2) ) )