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