given f being Arithmetic_Progression such that A1: ( difference f = 10 & ex p1, p2, p3, p4 being Prime ex i being Nat st
( p1,p2,p3,p4 are_mutually_distinct & p1 = f . i & p2 = f . (i + 1) & p3 = f . (i + 2) & p4 = f . (i + 3) ) ) ; :: thesis: contradiction
reconsider f = f as integer-valued Arithmetic_Progression by A1, LemmaIntProg;
consider p1, p2, p3, p4 being Prime, i being Nat such that
A2: ( p1,p2,p3,p4 are_mutually_distinct & p1 = f . i & p2 = f . (i + 1) & p3 = f . (i + 2) & p4 = f . (i + 3) ) by A1;
b1: p2 - p1 = difference f by A2, LemmaDiffConst;
p3 = f . ((i + 1) + 1) by A2;
then b2: p3 - p2 = difference f by A2, LemmaDiffConst;
p4 = f . ((i + 2) + 1) by A2;
then bb: p4 - p3 = difference f by A2, LemmaDiffConst;
K1: ( 3 divides p1 + 1 iff 3 divides (p1 + 1) + (3 * 3) ) by LemmaCong;
( 3 divides p1 + 2 iff 3 divides (p1 + 2) + (3 * 6) ) by LemmaCong;

per cases then ( p1 = 3 or p2 = 3 or p3 = 3 ) by b2, A1, b1, K1, ThreeConsecutive, LemmaDivides;

suppose aa: p1 = 3 ; :: thesis: contradiction

then p4 = 3 * 11 by bb, A1, b1, b2;
then 11 divides p4 ;
then not 33 is prime by aa, bb, A1, b1, b2;
hence contradiction by aa, bb, A1, b1, b2; :: thesis: verum

end;

suppose p2 = 3 ; :: thesis: contradiction

then p1 = 3 - 10 by A1, b1;
hence contradiction by INT_2:def 4; :: thesis: verum

end;

suppose p3 = 3 ; :: thesis: contradiction

then p2 = 3 - 10 by A1, b2;
hence contradiction by INT_2:def 4; :: thesis: verum

end;

end;