theorem Th78: :: POLYFORM:80

for p being polyhedron
for n being Nat st 1 < n & n < (dim p) + 2 holds
(alternating-f-vector p) . n = (alternating-proper-f-vector p) . (n - 1)