set aspcs = alternating-semi-proper-f-vector p;
set acs = alternating-f-vector p;
alternating-f-vector p = <*(- 1)*> ^ (alternating-semi-proper-f-vector p) by Th54;
then A1: Sum (alternating-f-vector p) = (- 1) + (Sum (alternating-semi-proper-f-vector p)) by Th21;
( p is eulerian implies Sum (alternating-f-vector p) = 0 )

proof

assume p is eulerian ; :: thesis: Sum (alternating-f-vector p) = 0
then Sum (alternating-f-vector p) = (- 1) + 1 by A1, Def30
.= 0 ;
hence Sum (alternating-f-vector p) = 0 ; :: thesis: verum

end;

hence ( p is eulerian iff Sum (alternating-f-vector p) = 0 ) by A1, Def30; :: thesis: verum