defpred S_{1}[ Nat] means ( 1 <= $1 & $1 <= F_{1}() & P_{1}[$1] );

assume ex i being Element of NAT st

( 1 <= i & i <= F_{1}() & P_{1}[i] )
; :: thesis: contradiction

then A3: ex k being Nat st S_{1}[k]
;

consider k being Nat such that

A4: ( S_{1}[k] & ( for k9 being Nat st S_{1}[k9] holds

k <= k9 ) ) from NAT_1:sch 5(A3);

assume ex i being Element of NAT st

( 1 <= i & i <= F

then A3: ex k being Nat st S

consider k being Nat such that

A4: ( S

k <= k9 ) ) from NAT_1:sch 5(A3);

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

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_{1}()
by A4, XXREAL_0:2;

hence contradiction by A2, A4, A6, A8, A7; :: thesis: verum

end;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

hence contradiction by A2, A4, A6, A8, A7; :: thesis: verum