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

per cases ( k = F₁() or k <> F₁() ) ;

suppose k = F₁() ; :: thesis: contradiction

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

end;

suppose k <> F₁() ; :: thesis: contradiction

then F₁() < k by A4, XXREAL_0:1;
then F₁() + 1 <= k by NAT_1:13;
then A5: (F₁() + 1) - 1 <= k - 1 by XREAL_1:11;
then reconsider k' = k - 1 as Element of NAT by INT_1:16;
A6: (k - 1) + 1 = k + 0 ;
A7: k' <= k' + 1 by NAT_1:11;
k' <> k' + 1 ;
then A8: k' < k by A7, XXREAL_0:1;
then A9: not S₁[k'] by A4;
k' < F₂() by A4, A8, XXREAL_0:2;
hence contradiction by A2, A4, A5, A6, A9; :: thesis: verum

end;

end;