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 Th89;
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 Th87;
0 = Sum (alternating-f-vector p) by A1, Def31
.= (((num-polytopes p,0 ) - (num-polytopes p,1)) + (num-polytopes p,2)) - 2 by A2, A3, Th6, Th83 ;
hence ((num-vertices p) - (num-edges p)) + (num-faces p) = 2 ; :: thesis: verum