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 k9 being Nat st S₁[k9] holds
k <= k9 ) ) 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:9;
then reconsider k9 = k - 1 as Element of NAT by Th3;
A6: k9 <> k9 + 1 ;
k9 <= k9 + 1 by NAT_1:11;
then A7: k9 < k by A6, XXREAL_0:1;
then A8: k9 < F₂() by A4, XXREAL_0:2;
A9: (k - 1) + 1 = k + 0 ;
not S₁[k9] by A4, A7;
hence contradiction by A2, A4, A5, A9, A8; :: thesis: verum

end;

end;