:: deftheorem defines num-edges POLYFORM:def 10 :
for p being polyhedron holds num-edges p = num-polytopes (p,1);