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