for p being polyhedron
for k being Integer holds
( not k -polytopes p is empty iff ( - 1 <= k & k <= dim p ) )