let p be polyhedron; for k being Integer st k = - 1 holds
dim (k -bounding-chain-space p) = 1
let k be Integer; ( k = - 1 implies dim (k -bounding-chain-space p) = 1 )
set T = 0 -boundary p;
set V = k -bounding-chain-space p;
assume A1:
k = - 1
; dim (k -bounding-chain-space p) = 1
card ([#] (k -bounding-chain-space p)) = 2
proof
[#] (k -bounding-chain-space p) c= [#] (k -chain-space p)
by VECTSP_4:def 2;
then
card ([#] (k -bounding-chain-space p)) c= card ([#] (k -chain-space p))
by CARD_1:11;
then A2:
card ([#] (k -bounding-chain-space p)) c= 2
by A1, Th53;
0 -polytopes p <> {}
by Th52;
then consider x being
object such that A3:
x in 0 -polytopes p
by XBOOLE_0:def 1;
reconsider x =
x as
Element of
0 -polytopes p by A3;
set v =
{x};
A4:
(0 -boundary p) . {x} = {{}}
by Th59;
reconsider v =
{x} as
Subset of
(0 -polytopes p) by A3, ZFMISC_1:31;
reconsider v =
v as
Element of
(0 -chain-space p) ;
A5:
dom (0 -boundary p) = [#] (0 -chain-space p)
by RANKNULL:7;
then
v in dom (0 -boundary p)
;
then A6:
{{}} in rng (0 -boundary p)
by A4, FUNCT_1:3;
(0 -boundary p) . (0. (0 -chain-space p)) =
0. (k -chain-space p)
by A1, RANKNULL:9
.=
{}
;
then
{} in rng (0 -boundary p)
by A5, FUNCT_1:3;
then A7:
{{},{{}}} c= rng (0 -boundary p)
by A6, ZFMISC_1:32;
card {{},{{}}} = 2
by CARD_2:57;
then A8:
2
c= card (rng (0 -boundary p))
by A7, CARD_1:11;
card (rng (0 -boundary p)) =
card ((0 -boundary p) .: ([#] (0 -chain-space p)))
by RELSET_1:22
.=
card ([#] (k -bounding-chain-space p))
by A1, RANKNULL:def 2
;
hence
card ([#] (k -bounding-chain-space p)) = 2
by A8, A2;
verum
end;
hence
dim (k -bounding-chain-space p) = 1
by RANKNULL:6; verum