defpred S₁[ Nat] means ( 1 <= $1 & $1 <= F₁() & P₁[$1] );
assume ex k being Element of NAT st S₁[k] ; :: thesis: contradiction
then A3: ex k being Nat st S₁[k] ;
A4: for l being Nat st S₁[l] holds
l <= F₁() ;
consider l being Nat such that
A5: S₁[l] and
A6: for n being Nat st S₁[n] holds
n <= l from NAT_1:sch 6(A4, A3);
A7: l + 1 >= 1 by NAT_1:12;
A8: l < F₁() by A1, A5, XXREAL_0:1;
then A9: l + 1 <= F₁() by NAT_1:13;

A10: now :: thesis: P₁[l + 1]

assume P₁[l + 1] ; :: thesis: contradiction
then l + 1 <= l by A6, A9, A7;
hence contradiction by XREAL_1:29; :: thesis: verum

end;

l in NAT by ORDINAL1:def 12;
hence contradiction by A2, A5, A8, A10; :: thesis: verum