defpred S₁[ Element of (k - 1) -polytopes p] means Sum (incidence-sequence $1,v) = 1. Z_2 ;
consider c being Subset of ((k - 1) -polytopes p) such that
A2: for x being Element of (k - 1) -polytopes p holds
( x in c iff ( S₁[x] & x in (k - 1) -polytopes p ) ) from POLYFORM:sch 1();
reconsider c = c as Element of ((k - 1) -chain-space p) ;
take c ; :: thesis: ( ( (k - 1) -polytopes p is empty implies c = 0. ((k - 1) -chain-space p) ) & ( not (k - 1) -polytopes p is empty implies for x being Element of (k - 1) -polytopes p holds
( x in c iff Sum (incidence-sequence x,v) = 1. Z_2 ) ) )
thus ( ( (k - 1) -polytopes p is empty implies c = 0. ((k - 1) -chain-space p) ) & ( not (k - 1) -polytopes p is empty implies for x being Element of (k - 1) -polytopes p holds
( x in c iff Sum (incidence-sequence x,v) = 1. Z_2 ) ) ) by A2; :: thesis: verum