let p be polyhedron; :: thesis: card ([#] ((- 1) -chain-space p)) = 2
(- 1) -polytopes p = {{}} by Def5;
then card ((- 1) -polytopes p) = 1 by CARD_1:50;
then card ([#] ((- 1) -chain-space p)) = exp (2,1) by BSPACE:43
.= 2 by CARD_2:40 ;
hence card ([#] ((- 1) -chain-space p)) = 2 ; :: thesis: verum