let p be polyhedron; :: thesis: [#] ((- 1) -chain-space p) = {{},{{}}}
(- 1) -polytopes p = {{}} by Def5;
hence [#] ((- 1) -chain-space p) = {{},{{}}} by ZFMISC_1:24; :: thesis: verum