theorem Th84: :: POLYFORM:86

for p being polyhedron st dim p = 3 holds
Sum (alternating-proper-f-vector p) = ((num-polytopes (p,0)) - (num-polytopes (p,1))) + (num-polytopes (p,2))