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 Th86;
assume A2: dim p = 1 ; :: thesis: num-vertices p = 2
0 = Sum (alternating-f-vector p) by A1
.= (Sum (alternating-proper-f-vector p)) - 2 by A2, Th3, Th80
.= (num-polytopes (p,0)) - 2 by A2, Th82 ;
hence num-vertices p = 2 ; :: thesis: verum