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