reconsider n9 = F₁() as Element of NAT by ORDINAL1:def 12;
defpred S₁[ Nat] means ( $1 <= F₁() & P₁[$1] );
assume ex k being Element of NAT st
( k <= F₁() & P₁[k] ) ; :: thesis: contradiction
then A3: ex k being Nat st S₁[k] ;
A4: for l being Nat st S₁[l] holds
l <= n9 ;
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 in NAT by ORDINAL1:def 12;
A8: l < F₁() by A1, A5, XXREAL_0:1;
then l + 1 <= F₁() by NAT_1:13;
then P₁[l + 1] by A6, XREAL_1:29;
hence contradiction by A2, A5, A8, A7; :: thesis: verum