defpred S₁[ Integer] means for i2 being Integer st $1 = - i2 holds
P₁[i2];
A3: for i2 being Integer st - F₁() <= i2 & S₁[i2] holds
S₁[i2 + 1]

proof

let i2 be Integer; :: thesis: ( - F₁() <= i2 & S₁[i2] implies S₁[i2 + 1] )
assume that
A4: - F₁() <= i2 and
A5: S₁[i2] ; :: thesis: S₁[i2 + 1]
let i3 be Integer; :: thesis: ( i2 + 1 = - i3 implies P₁[i3] )
assume A6: i2 + 1 = - i3 ; :: thesis: P₁[i3]
then A7: i2 = - (i3 + 1) ;
- ((- i3) - 1) <= - (- F₁()) by A4, A6, XREAL_1:24;
then P₁[(i3 + 1) - 1] by A2, A5, A7;
hence P₁[i3] ; :: thesis: verum

end;

let i0 be Integer; :: thesis: ( i0 <= F₁() implies P₁[i0] )
assume i0 <= F₁() ; :: thesis: P₁[i0]
then A8: - F₁() <= - i0 by XREAL_1:24;
A9: S₁[ - F₁()] by A1;
for i2 being Integer st - F₁() <= i2 holds
S₁[i2] from INT_1:sch 2(A9, A3);
hence P₁[i0] by A8; :: thesis: verum