for p being polyhedron holds not ((dim p) - 1) -polytopes p is empty