for p being polyhedron
for k being Integer st k < dim p holds
k - 1 < dim p by XREAL_1:146, XXREAL_0:2;