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 Th61;
reconsider C = [#] ((dim p) -chain-space p) as finite set ;
A2: {p} in C by Th63;
ex a, b being object st
( a <> b & C = {a,b} ) by A1, CARD_2:60;
hence [#] ((dim p) -chain-space p) = {(0. ((dim p) -chain-space p)),{p}} by A2, Th1; :: thesis: verum