let p be polyhedron; :: thesis: for x being Element of 0 -polytopes p holds (0 -boundary p) . {x} = {{}}
reconsider minusone = 0 - 1 as Integer ;
let x be Element of 0 -polytopes p; :: thesis: (0 -boundary p) . {x} = {{}}
set T = 0 -boundary p;
not 0 -polytopes p is empty by Th52;
then reconsider v = {x} as Subset of (0 -polytopes p) by ZFMISC_1:31;
(0 - 1) -polytopes p = {{}} by Def5;
then reconsider null = {} as Element of (0 - 1) -polytopes p by TARSKI:def 1;
reconsider v = v as Element of (0 -chain-space p) ;
reconsider bv = Boundary v as Element of (minusone -chain-space p) ;
A1: bv c= {null}
proof
A2: [#] (minusone -chain-space p) = {{},{{}}} by Th54;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in bv or y in {null} )
assume A3: y in bv ; :: thesis: y in {null}
per cases ( bv = {} or bv = {{}} ) by A2, TARSKI:def 2;
suppose bv = {} ; :: thesis: y in {null}
hence y in {null} by A3; :: thesis: verum
end;
suppose bv = {{}} ; :: thesis: y in {null}
hence y in {null} by A3; :: thesis: verum
end;
end;
end;
not minusone -polytopes p is empty by Def5;
then ( null in bv iff Sum (incidence-sequence (null,v)) = 1. Z_2 ) by Def17;
then A4: {null} c= bv by Th58, ZFMISC_1:31;
(0 -boundary p) . v = Boundary v by Def18;
hence (0 -boundary p) . {x} = {{}} by A4, A1; :: thesis: verum