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