let p be polyhedron; :: thesis: ( dim p = 0 implies p is eulerian )
set d = dim p;
set apcs = alternating-proper-f-vector p;
assume A1: dim p = 0 ; :: thesis: p is eulerian
then (- 1) |^ ((dim p) + 1) = - 1 ;
then A2: 1 + ((- 1) |^ ((dim p) + 1)) = 0 ;
len (alternating-proper-f-vector p) = 0 by A1, Def27;
then alternating-proper-f-vector p = <*> INT ;
hence p is eulerian by A2, GR_CY_1:3; :: thesis: verum