:: deftheorem defines num-polytopes POLYFORM:def 8 :
for p being polyhedron
for k being Integer holds num-polytopes (p,k) = card (k -polytopes p);