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 TARSKI:def 1;
then [x,c] in dom ([:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2)) by ZFMISC_1:87;
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:3;
then ([:(((dim p) - 1) -polytopes p),{p}:] --> (1. Z_2)) . (x,c) in {(1. Z_2)} by FUNCOP_1:8;
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