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 ) )
A1: (- 1) + 1 = 0 ;
assume - 1 < k ; :: thesis: ( not k < dim p or ( k + 1 is Nat & 1 <= k + 1 & k + 1 <= dim p ) )
then A2: 0 < k + 1 by A1, XREAL_1:6;
then reconsider n = k + 1 as Element of NAT by INT_1:3;
A3: ( n is Nat & 0 + 1 = 1 ) ;
assume k < dim p ; :: thesis: ( k + 1 is Nat & 1 <= k + 1 & k + 1 <= dim p )
hence ( k + 1 is Nat & 1 <= k + 1 & k + 1 <= dim p ) by A2, A3, INT_1:7; :: thesis: verum