per cases ( (k - 1) -polytopes p is empty or not (k - 1) -polytopes p is empty ) ;

suppose A1: (k - 1) -polytopes p is empty ; :: thesis: ex b₁ being Element of ((k - 1) -chain-space p) st
( ( (k - 1) -polytopes p is empty implies b₁ = 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 b₁ iff Sum (incidence-sequence x,v) = 1. Z_2 ) ) )

take 0. ((k - 1) -chain-space p) ; :: thesis: ( ( (k - 1) -polytopes p is empty implies 0. ((k - 1) -chain-space p) = 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 0. ((k - 1) -chain-space p) iff Sum (incidence-sequence x,v) = 1. Z_2 ) ) )
thus ( ( (k - 1) -polytopes p is empty implies 0. ((k - 1) -chain-space p) = 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 0. ((k - 1) -chain-space p) iff Sum (incidence-sequence x,v) = 1. Z_2 ) ) ) by A1; :: thesis: verum

end;

suppose not (k - 1) -polytopes p is empty ; :: thesis: ex b₁ being Element of ((k - 1) -chain-space p) st
( ( (k - 1) -polytopes p is empty implies b₁ = 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 b₁ iff Sum (incidence-sequence x,v) = 1. Z_2 ) ) )

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

end;

end;