let p be polyhedron; :: thesis: for x being Element of ((dim p) - 1) -polytopes p
for c being Element of (dim p) -polytopes p st c = p holds
incidence-value x,c = 1. Z_2
set f = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2 );
let x be Element of ((dim p) - 1) -polytopes p; :: thesis: for c being Element of (dim p) -polytopes p st c = p holds
incidence-value x,c = 1. Z_2
let c be Element of (dim p) -polytopes p; :: thesis: ( c = p implies incidence-value x,c = 1. Z_2 )
assume c = p ; :: thesis: incidence-value x,c = 1. Z_2
then ( dom ([:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2 )) = [:(((dim p) - 1) -polytopes p),{p}:] & c in {p} ) by FUNCOP_1:19, TARSKI:def 1;
then [x,c] in dom ([:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2 )) by ZFMISC_1:106;
then ([:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2 )) . x,c in rng ([:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2 )) by FUNCT_1:12;
then ([:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2 )) . x,c in {(1. Z_2 )} by FUNCOP_1:14;
then A1: ([:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2 )) . x,c = 1. Z_2 by TARSKI:def 1;
eta p,(dim p) = [:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2 ) by Def6;
hence incidence-value x,c = 1. Z_2 by A1, Def13; :: thesis: verum