:: deftheorem Def2 defines polyhedron_2 POLYFORM:def 2 :
for p being PolyhedronStr holds
( p is polyhedron_2 iff for n being Nat st 1 <= n & n < len the PolytopsF of p holds
the IncidenceF of p . n is incidence-matrix of (rng ( the PolytopsF of p . n)),(rng ( the PolytopsF of p . (n + 1))) );