let f be increasing Arithmetic_Progression; :: thesis: ( ( for i being Nat holds f . i is Prime ) implies f . 1 > 2 )
assume A1: for i being Nat holds f . i is Prime ; :: thesis: f . 1 > 2
A2: f . 1 > f . 0 by SEQM_3:1;
f . 0 is Prime by A1;
then B2: f . 0 > 1 by INT_2:def 4;
reconsider f0 = f . 0 as Prime by A1;
f0 >= 1 + 1 by B2, NAT_1:13;
hence f . 1 > 2 by A2, XXREAL_0:2; :: thesis: verum