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