let p be polyhedron; :: thesis: for k being Integer st - 1 < k & k < dim p holds
( k + 1 is Nat & 1 <= k + 1 & k + 1 <= dim p )
let k be Integer; :: thesis: ( - 1 < k & k < dim p implies ( k + 1 is Nat & 1 <= k + 1 & k + 1 <= dim p ) )
assume A1: - 1 < k ; :: thesis: ( not k < dim p or ( k + 1 is Nat & 1 <= k + 1 & k + 1 <= dim p ) )
assume A2: k < dim p ; :: thesis: ( k + 1 is Nat & 1 <= k + 1 & k + 1 <= dim p )
(- 1) + 1 = 0 ;
then A3: 0 < k + 1 by A1, XREAL_1:8;
then reconsider n = k + 1 as Element of NAT by INT_1:16;
A4: n is Nat ;
0 + 1 = 1 ;
hence ( k + 1 is Nat & 1 <= k + 1 & k + 1 <= dim p ) by A2, A3, A4, INT_1:20; :: thesis: verum