defpred S₁[ Nat] means P₁[F₁() - $1];
consider i1 being Integer such that
A3: P₁[i1] by A2;
ex k being Element of NAT st i1 = F₁() - k by A1, A3, Lm7;
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
i1 <= i0 ) )
for i1 being Integer st P₁[i1] holds
i1 <= i0

proof

let i1 be Integer; :: thesis: ( P₁[i1] implies i1 <= i0 )
assume A6: P₁[i1] ; :: thesis: i1 <= i0
then consider n being Element of NAT such that
A7: F₁() - n = i1 by A1, Lm7;
l <= n by A5, A6, A7;
then (F₁() + (- i0)) - F₁() <= (F₁() - i1) - F₁() by A7, XREAL_1:11;
then - i0 <= (F₁() + (- i1)) - F₁() ;
hence i1 <= i0 by XREAL_1:26; :: thesis: verum

end;

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