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 Th51;
then A1: Sum (alternating-f-vector p) = (- 1) + (Sum (alternating-semi-proper-f-vector p)) by Th18;
thus ( p is eulerian iff Sum (alternating-f-vector p) = 0 ) by A1; :: thesis: verum