:: deftheorem defines dim POLYFORM:def 4 :
for p being polyhedron holds dim p = len the PolytopsF of p;