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: ( 0 <= k & k <= dim p ) by A1;
A4: eta p,k = [:{{} },(0 -polytopes p):] --> (1. Z_2 ) by A1, Def6;
A5: {} in {{} } by TARSKI:def 1;
not 0 -polytopes p is empty by A3, Th26;
then A6: [{} ,x] in [:{{} },(0 -polytopes p):] by A1, A5, ZFMISC_1:106;
incidence-value e,x = (eta p,k) . e,x by A3, Def13
.= 1. Z_2 by A2, A4, A6, FUNCOP_1:13 ;
hence incidence-value e,x = 1. Z_2 ; :: thesis: verum