:: deftheorem defines num-faces POLYFORM:def 11 :
for p being polyhedron holds num-faces p = num-polytopes (p,2);