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:30;
then card ([#] ((- 1) -chain-space p)) = exp (2,1) by BSPACE:42
.= 2 by CARD_2:27 ;
hence card ([#] ((- 1) -chain-space p)) = 2 ; :: thesis: verum