let p be polyhedron; :: thesis: {p} is Element of ((dim p) -chain-space p)
(dim p) -polytopes p = {p} by Def5;
hence {p} is Element of ((dim p) -chain-space p) ; :: thesis: verum