for p being polyhedron holds (dim p) -polytope-seq p = <*p*> by Def7;