:: deftheorem defines num-vertices POLYFORM:def 9 :
for p being polyhedron holds num-vertices p = num-polytopes (p,0);