let f be increasing Arithmetic_Progression; :: thesis: ( ( for i being Nat holds f . i is Prime ) implies difference f is even Nat )
assume A1: for i being Nat holds f . i is Prime ; :: thesis: difference f is even Nat
f . 2 > f . 1 by SEQM_3:1;
then f . 2 > 2 by A1, FirstAPPrime, XXREAL_0:2;
then reconsider f2 = f . 2, f1 = f . 1 as 2 _greater Prime by NAT_6:def 1, A1, FirstAPPrime;
C5: f2 - f1 > 0 by SEQM_3:1, XREAL_1:50;
(f . (1 + 1)) - (f . 1) = (f . 1) - (f . 0) by NUMBER06:5;
hence difference f is even Nat by C5, NUMBER06:def 5; :: thesis: verum