let p be polyhedron; :: thesis: for k being Integer
for x being Element of k -polytopes p
for e being Element of (k - 1) -polytopes p st k = 0 & e = {} holds
incidence-value (e,x) = 1. Z_2
let k be Integer; :: thesis: for x being Element of k -polytopes p
for e being Element of (k - 1) -polytopes p st k = 0 & e = {} holds
incidence-value (e,x) = 1. Z_2
let x be Element of k -polytopes p; :: thesis: for e being Element of (k - 1) -polytopes p st k = 0 & e = {} holds
incidence-value (e,x) = 1. Z_2
let e be Element of (k - 1) -polytopes p; :: thesis: ( k = 0 & e = {} implies incidence-value (e,x) = 1. Z_2 )
assume that
A1: k = 0 and
A2: e = {} ; :: thesis: incidence-value (e,x) = 1. Z_2
A3: eta (p,k) = [:{{}},(0 -polytopes p):] --> (1. Z_2) by A1, Def6;
A4: k <= dim p by A1;
then ( {} in {{}} & not 0 -polytopes p is empty ) by Th23, TARSKI:def 1;
then A5: [{},x] in [:{{}},(0 -polytopes p):] by A1, ZFMISC_1:87;
incidence-value (e,x) = (eta (p,k)) . (e,x) by A1, A4, Def13
.= 1. Z_2 by A2, A3, A5, FUNCOP_1:7 ;
hence incidence-value (e,x) = 1. Z_2 ; :: thesis: verum