defpred S₁[ Nat] means ( 1 <= $1 & $1 <= F₁() & P₁[$1] );
assume ex i being Element of NAT st
( 1 <= i & i <= F₁() & P₁[i] ) ; :: thesis: contradiction
then A3: ex k being Nat st S₁[k] ;
consider k being Nat such that
A4: ( S₁[k] & ( for k9 being Nat st S₁[k9] holds
k <= k9 ) ) from NAT_1:sch 5(A3);

per cases ( k = 1 or k <> 1 ) ;

suppose k = 1 ; :: thesis: contradiction

hence contradiction by A1, A4; :: thesis: verum

end;

suppose A5: k <> 1 ; :: thesis: contradiction

1 - 1 <= k - 1 by A4, XREAL_1:9;
then reconsider k9 = k - 1 as Element of NAT by INT_1:3;
A6: (k - 1) + 1 = k + 0 ;
1 < k by A4, A5, XXREAL_0:1;
then A7: 1 <= k9 by A6, NAT_1:13;
( k9 <= k9 + 1 & k9 <> k9 + 1 ) by NAT_1:11;
then A8: k9 < k by XXREAL_0:1;
then k9 < F₁() by A4, XXREAL_0:2;
hence contradiction by A2, A4, A6, A8, A7; :: thesis: verum

end;

end;