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:11;
(dim p) - 1 <= dim p by XREAL_1:148;
hence not ((dim p) - 1) -polytopes p is empty by A1, Th26; :: thesis: verum