let p be polyhedron; :: thesis: 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) )
set V = (dim p) -chain-space p;
let x, y be Element of ((dim p) -chain-space p); :: thesis: ( not x <> y or x = 0. ((dim p) -chain-space p) or y = 0. ((dim p) -chain-space p) )
assume A1: x <> y ; :: thesis: ( x = 0. ((dim p) -chain-space p) or y = 0. ((dim p) -chain-space p) )
assume x <> 0. ((dim p) -chain-space p) ; :: thesis: y = 0. ((dim p) -chain-space p)
then A2: x = {p} by Th66;
assume y <> 0. ((dim p) -chain-space p) ; :: thesis: contradiction
hence contradiction by A1, A2, Th66; :: thesis: verum