theorem Th26: :: POLYFORM:28
for p being polyhedron
for k being Integer holds len (k -polytope-seq p) = num-polytopes (p,k)