let p be polyhedron; :: thesis:
let k be Integer; :: thesis:
let c be Element of (k -chain-space p); :: thesis:
let x be Element of (k - 1) -polytopes p; :: thesis:
set b = Boundary c;

per cases ) -polytopes p is empty or not (k - 1) -polytopes p is empty ) ;

suppose A1: (k - 1) -polytopes p is empty ; :: thesis:

set iscx = incidence-sequence (x,c);
incidence-sequence (x,c) = <*> the carrier of Z_2 by A1, Def16;
then A2: Sum (incidence-sequence (x,c)) = 0. Z_2 by RLVECT_1:43;
Boundary c = 0. ((k - 1) -chain-space p) by A1;
hence (Boundary c) @ x = Sum (incidence-sequence (x,c)) by A2, BSPACE:14; :: thesis:

end;

suppose A3: not (k - 1) -polytopes p is empty ; :: thesis:

then A4: ( x in Boundary c iff Sum (incidence-sequence (x,c)) = 1. Z_2 ) by Def17;

suppose x in Boundary c ; :: thesis:

hence (Boundary c) @ x = Sum (incidence-sequence (x,c)) by A4, BSPACE:def 3; :: thesis:

end;

suppose A5: not x in Boundary c ; :: thesis:

then Sum (incidence-sequence (x,c)) <> 1. Z_2 by A3, Def17;
then Sum (incidence-sequence (x,c)) = 0. Z_2 by BSPACE:8;
hence (Boundary c) @ x = Sum (incidence-sequence (x,c)) by A5, BSPACE:def 3; :: thesis:

end;

end;

end;

end;