:: deftheorem Def26 defines alternating-f-vector POLYFORM:def 26 :
for p being polyhedron
for b₂ being FinSequence of INT holds
( b₂ = alternating-f-vector p iff ( len b₂ = (dim p) + 2 & ( for k being Nat st 1 <= k & k <= (dim p) + 2 holds
b₂ . k = ((- 1) |^ k) * (num-polytopes (p,(k - 2))) ) ) );