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