let k, n be Nat; ( k < n & 3 <= n & not k + 1 < n implies 2 <= k )
assume that
A1:
k < n
and
A2:
3 <= n
; ( k + 1 < n or 2 <= k )
assume A3:
k + 1 >= n
; 2 <= k
k + 1 <= n
by A1, NAT_1:13;
then
3 <= k + 1
by A2, A3, XXREAL_0:1;
then
3 - 1 <= (k + 1) - 1
by XREAL_1:9;
hence
2 <= k
; verum