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