theorem Th83: :: POLYFORM:85

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