theorem :: NUMBER06:50

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