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