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