let p be polyhedron; :: thesis: ( dim p = 2 implies Sum (alternating-proper-f-vector p) = (num-polytopes (p,0)) - (num-polytopes (p,1)) )
reconsider t = 2 as Nat ;
reconsider o = 1 as Nat ;
set apcs = alternating-proper-f-vector p;
reconsider apcso = (alternating-proper-f-vector p) . o as Integer ;
reconsider apcst = (alternating-proper-f-vector p) . t as Integer ;
assume A1: dim p = 2 ; :: thesis: Sum (alternating-proper-f-vector p) = (num-polytopes (p,0)) - (num-polytopes (p,1))
then A2: ( (alternating-proper-f-vector p) . o = ((- 1) |^ (o + 1)) * (num-polytopes (p,(o - 1))) & (alternating-proper-f-vector p) . t = ((- 1) |^ (t + 1)) * (num-polytopes (p,(t - 1))) ) by Def27;
A3: ( (- 1) |^ (o + 1) = 1 & (- 1) |^ (t + 1) = - 1 ) by Th4, Th7, Th8;
len (alternating-proper-f-vector p) = 2 by A1, Def27;
then alternating-proper-f-vector p = <*apcso,apcst*> by FINSEQ_1:44;
then Sum (alternating-proper-f-vector p) = apcso + apcst by RVSUM_1:77
.= (num-polytopes (p,0)) - (num-polytopes (p,1)) by A2, A3 ;
hence Sum (alternating-proper-f-vector p) = (num-polytopes (p,0)) - (num-polytopes (p,1)) ; :: thesis: verum