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
A1: 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 A1; :: thesis: verum