let p be polyhedron; dim (((dim p) - 1) -bounding-chain-space p) = 1
set d = dim p;
set T = (dim p) -boundary p;
set U = (dim p) -chain-space p;
set V = ((dim p) - 1) -bounding-chain-space p;
A1: card ([#] (((dim p) - 1) -bounding-chain-space p)) =
card (((dim p) -boundary p) .: ([#] ((dim p) -chain-space p)))
by RANKNULL:def 2
.=
card (rng ((dim p) -boundary p))
by RELSET_1:22
;
A2: card (dom ((dim p) -boundary p)) =
card ([#] ((dim p) -chain-space p))
by RANKNULL:7
.=
2
by Th61
;
(dim p) -boundary p is one-to-one
by Th75;
then
card ([#] (((dim p) - 1) -bounding-chain-space p)) = 2
by A1, A2, CARD_1:70;
hence
dim (((dim p) - 1) -bounding-chain-space p) = 1
by RANKNULL:6; verum