let p be polyhedron; :: thesis: ((dim p) -boundary p) . {p} = ((dim p) - 1) -polytopes p
reconsider c = {p} as Element of ((dim p) -chain-space p) by Th62;
set T = (dim p) -boundary p;
set X = ((dim p) - 1) -polytopes p;
reconsider d = ((dim p) - 1) -polytopes p as Element of (((dim p) - 1) -chain-space p) by ZFMISC_1:def 1;
reconsider Tc = ((dim p) -boundary p) . c as Element of (((dim p) - 1) -chain-space p) ;
for x being Element of ((dim p) - 1) -polytopes p holds
( x in Tc iff x in d )
proof
let x be Element of ((dim p) - 1) -polytopes p; :: thesis: ( x in Tc iff x in d )
thus ( x in Tc implies x in d ) ; :: thesis: ( x in d implies x in Tc )
thus ( x in d implies x in Tc ) :: thesis: verum
proof
assume x in d ; :: thesis: x in Tc
Sum (incidence-sequence (x,c)) = 1. Z_2 by Th73;
then x in Boundary c by Def17;
hence x in Tc by Def18; :: thesis: verum
end;
end;
hence ((dim p) -boundary p) . {p} = ((dim p) - 1) -polytopes p by SUBSET_1:3; :: thesis: verum