for p being polyhedron
for x, y being Element of ((dim p) -chain-space p) holds
( not x <> y or x = 0. ((dim p) -chain-space p) or y = 0. ((dim p) -chain-space p) )