let p be polyhedron; :: thesis: not ((dim p) - 1) -polytopes p is empty
set n = (dim p) - 1;
A1: - 1 <= (dim p) - 1

proof

0 - 1 = - 1 ;
hence - 1 <= (dim p) - 1 by XREAL_1:11; :: thesis: verum

end;

(dim p) - 1 <= dim p by XREAL_1:148;
hence not ((dim p) - 1) -polytopes p is empty by A1, Th26; :: thesis: verum