let p be polyhedron; :: thesis: for c being Element of ((dim p) -chain-space p)
for x being Element of (dim p) -polytopes p st c = {p} holds
c @ x = 1. Z_2
A1: (dim p) -polytopes p = {p} by Def5;
let c be Element of ((dim p) -chain-space p); :: thesis: for x being Element of (dim p) -polytopes p st c = {p} holds
c @ x = 1. Z_2
let x be Element of (dim p) -polytopes p; :: thesis: ( c = {p} implies c @ x = 1. Z_2 )
assume c = {p} ; :: thesis: c @ x = 1. Z_2
hence c @ x = 1. Z_2 by A1, BSPACE:def 3; :: thesis: verum