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