defpred S₁[ Nat] means P₁[F₁() + $1];
consider i1 being Integer such that
A3: P₁[i1] by A2;
ex k being Nat st F₁() + k = i1 by A1, A3, Lm5;
then A4: ex k being Nat st S₁[k] by A3;
consider l being Nat such that
A5: ( S₁[l] & ( for n being Nat st S₁[n] holds
l <= n ) ) from NAT_1:sch 5(A4);
take i0 = F₁() + l; :: thesis: ( P₁[i0] & ( for i1 being Integer st P₁[i1] holds
i0 <= i1 ) )
for i1 being Integer st P₁[i1] holds
i0 <= i1

proof

let i1 be Integer; :: thesis: ( P₁[i1] implies i0 <= i1 )
assume A6: P₁[i1] ; :: thesis: i0 <= i1
then ex n being Nat st F₁() + n = i1 by A1, Lm5;
then i0 - F₁() <= i1 - F₁() by A5, A6;
hence i0 <= i1 by XREAL_1:9; :: thesis: verum

end;

hence ( P₁[i0] & ( for i1 being Integer st P₁[i1] holds
i0 <= i1 ) ) by A5; :: thesis: verum