let p be polyhedron; :: thesis: ( p is simply-connected & dim p = 1 implies num-vertices p = 2 )
set acs = alternating-f-vector p;
set apcs = alternating-proper-f-vector p;
assume p is simply-connected ; :: thesis: ( not dim p = 1 or num-vertices p = 2 )
then A1: p is eulerian by Th89;
assume A2: dim p = 1 ; :: thesis: num-vertices p = 2
0 = Sum (alternating-f-vector p) by A1, Def31
.= (Sum (alternating-proper-f-vector p)) - 2 by A2, Th4, Th83
.= (num-polytopes p,0 ) - 2 by A2, Th85 ;
hence num-vertices p = 2 ; :: thesis: verum