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 Th89;
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 Th86;
0 = Sum (alternating-f-vector p) by A1, Def31
.= (num-polytopes p,0 ) - (num-polytopes p,1) by A2, A3, Th5, Th84 ;
hence num-vertices p = num-edges p ; :: thesis: verum