let p be polyhedron; :: thesis: for k being Integer holds num-polytopes (p,k) = dim (k -chain-space p)
let k be Integer; :: thesis: num-polytopes (p,k) = dim (k -chain-space p)
set n = dim (k -chain-space p);
singletons (k -polytopes p) is Basis of (k -chain-space p) by BSPACE:40;
then dim (k -chain-space p) = card (singletons (k -polytopes p)) by VECTSP_9:def 1;
hence num-polytopes (p,k) = dim (k -chain-space p) by BSPACE:41; :: thesis: verum