let p be polyhedron; :: thesis: num-polytopes (p,(- 1)) = 1
reconsider minusone = - 1 as Integer ;
minusone -polytopes p = {{}} by Def5;
hence num-polytopes (p,(- 1)) = 1 by CARD_1:30; :: thesis: verum