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