let p be polyhedron; :: thesis: not ((dim p) - 1) -polytopes p is empty
set n = (dim p) - 1;
0 - 1 = - 1 ;
then A1: - 1 <= (dim p) - 1 by XREAL_1:9;
(dim p) - 1 <= dim p by XREAL_1:146;
hence not ((dim p) - 1) -polytopes p is empty by A1, Th23; :: thesis: verum