:: deftheorem Def5 defines -polytopes POLYFORM:def 5 :
for p being polyhedron
for k being Integer
for b₃ being finite set holds
( b₃ = k -polytopes p iff ( ( k < - 1 implies b₃ = {} ) & ( k = - 1 implies b₃ = {{}} ) & ( - 1 < k & k < dim p implies b₃ = rng ( the PolytopsF of p . (k + 1)) ) & ( k = dim p implies b₃ = {p} ) & ( k > dim p implies b₃ = {} ) ) );