:: deftheorem defines polyhedron_1 POLYFORM:def 1 :
for p being PolyhedronStr holds
( p is polyhedron_1 iff len the IncidenceF of p = (len the PolytopsF of p) - 1 );