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