let p be polyhedron; :: thesis: ( p is simply-connected & dim p = 2 implies num-vertices p = num-edges p )
set s = (num-polytopes (p,0)) - (num-polytopes (p,1));
set c = alternating-f-vector p;
assume p is simply-connected ; :: thesis: ( not dim p = 2 or num-vertices p = num-edges p )
then A1: p is eulerian by Th86;
assume A2: dim p = 2 ; :: thesis: num-vertices p = num-edges p
then A3: (num-polytopes (p,0)) - (num-polytopes (p,1)) = Sum (alternating-proper-f-vector p) by Th83;
0 = Sum (alternating-f-vector p) by A1
.= (num-polytopes (p,0)) - (num-polytopes (p,1)) by A2, A3, Th4, Th81 ;
hence num-vertices p = num-edges p ; :: thesis: verum