defpred S1[ Nat] means P1[F1() + $1];
consider i1 being Integer such that
A3: P1[i1] by A2;
ex k being Nat st F1() + k = i1 by A1, A3, Lm5;
then A4: ex k being Nat st S1[k] by A3;
consider l being Nat such that
A5: ( S1[l] & ( for n being Nat st S1[n] holds
l <= n ) ) from NAT_1:sch 5(A4);
 take i0 = F1() + l; :: thesis: ( P1[i0] & ( for i1 being Integer st P1[i1] holds
i0 <= i1 ) )
for i1 being Integer st P1[i1] holds
i0 <= i1
proof
let i1 be Integer; :: thesis: ( P1[i1] implies i0 <= i1 )
assume A6: P1[i1] ; :: thesis: i0 <= i1
then ex n being Nat st F1() + n = i1 by A1, Lm5;
then i0 - F1() <= i1 - F1() by A5, A6;
hence i0 <= i1 by XREAL_1:9; :: thesis: verum
end;
hence ( P1[i0] & ( for i1 being Integer st P1[i1] holds
i0 <= i1 ) ) by A5; :: thesis: verum