defpred S1[ Integer] means for i2 being Integer st $1 = - i2 holds
P1[i2];
A3: for i2 being Integer st - F1() <= i2 & S1[i2] holds
S1[i2 + 1]
proof
let i2 be Integer; :: thesis: ( - F1() <= i2 & S1[i2] implies S1[i2 + 1] )
assume that
A4: - F1() <= i2 and
A5: S1[i2] ; :: thesis: S1[i2 + 1]
let i3 be Integer; :: thesis: ( i2 + 1 = - i3 implies P1[i3] )
assume A6: i2 + 1 = - i3 ; :: thesis: P1[i3]
then A7: i2 = - (i3 + 1) ;
- ((- i3) - 1) <= - (- F1()) by A4, A6, XREAL_1:24;
then P1[(i3 + 1) - 1] by A2, A5, A7;
hence P1[i3] ; :: thesis: verum
end;
let i0 be Integer; :: thesis: ( i0 <= F1() implies P1[i0] )
assume i0 <= F1() ; :: thesis: P1[i0]
then A8: - F1() <= - i0 by XREAL_1:24;
A9: S1[ - F1()] by A1;
for i2 being Integer st - F1() <= i2 holds
S1[i2] from INT_1:sch 2(A9, A3);
 hence P1[i0] by A8; :: thesis: verum