let p be polyhedron; :: thesis: {p} in [#] ((dim p) -chain-space p)
{p} is Element of ((dim p) -chain-space p) by Th62;
hence {p} in [#] ((dim p) -chain-space p) ; :: thesis: verum