:: deftheorem Def7 defines -polytope-seq POLYFORM:def 7 :
for p being polyhedron
for k being Integer
for b₃ being FinSequence holds
( b₃ = k -polytope-seq p iff ( ( k < - 1 implies b₃ = <*> {} ) & ( k = - 1 implies b₃ = <*{}*> ) & ( - 1 < k & k < dim p implies b₃ = the PolytopsF of p . (k + 1) ) & ( k = dim p implies b₃ = <*p*> ) & ( k > dim p implies b₃ = <*> {} ) ) );