let p be polyhedron; :: thesis: [#] ((dim p) -chain-space p) = {(0. ((dim p) -chain-space p)),{p}}
set V = (dim p) -chain-space p;
set C = [#] ((dim p) -chain-space p);
A1: card ([#] ((dim p) -chain-space p)) = 2 by Th64;
reconsider C = [#] ((dim p) -chain-space p) as finite set ;
consider a, b being set such that
A2: a <> b and
A3: C = {a,b} by A1, CARD_2:79;
{p} in C by Th66;
hence [#] ((dim p) -chain-space p) = {(0. ((dim p) -chain-space p)),{p}} by A2, A3, Th1; :: thesis: verum