theorem :: NUMBER06:49

for f being Arithmetic_Progression
for p1, p2, p3 being Prime st difference f = 10 & ex i being Nat st
( p1 = f . i & p2 = f . (i + 1) & p3 = f . (i + 2) ) holds
p1 = 3