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:41;
then dim (k -chain-space p) = card (singletons (k -polytopes p)) by VECTSP_9:def 2;
hence num-polytopes p,k = dim (k -chain-space p) by BSPACE:42; :: thesis: verum