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:50; :: thesis: verum