let p be polyhedron; :: thesis: for x being Element of 0 -polytopes p holds (0 -boundary p) . {x} = {{} }
let x be Element of 0 -polytopes p; :: thesis: (0 -boundary p) . {x} = {{} }
set T = 0 -boundary p;
reconsider minusone = 0 - 1 as Integer ;
not 0 -polytopes p is empty by Th55;
then reconsider v = {x} as Subset of (0 -polytopes p) by ZFMISC_1:37;
reconsider v = v as Element of (0 -chain-space p) ;
A1: (0 -boundary p) . v = Boundary v by Def18;
reconsider bv = Boundary v as Element of (minusone -chain-space p) ;
A2: not minusone -polytopes p is empty by Def5;
(0 - 1) -polytopes p = {{} } by Def5;
then reconsider null = {} as Element of (0 - 1) -polytopes p by TARSKI:def 1;
( null in bv iff Sum (incidence-sequence null,v) = 1. Z_2 ) by A2, Def17;
then A3: {null} c= bv by Th61, ZFMISC_1:37;
bv c= {null}

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in bv or y in {null} )
assume A4: y in bv ; :: thesis: y in {null}
A5: [#] (minusone -chain-space p) = {{} ,{{} }} by Th57;

per cases ( bv = {} or bv = {{} } ) by A5, TARSKI:def 2;

suppose bv = {} ; :: thesis: y in {null}

hence y in {null} by A4; :: thesis: verum

end;

suppose bv = {{} } ; :: thesis: y in {null}

hence y in {null} by A4; :: thesis: verum

end;

end;

end;

hence (0 -boundary p) . {x} = {{} } by A1, A3, XBOOLE_0:def 10; :: thesis: verum