let p be polyhedron; :: thesis: for x being Element of ((dim p) -chain-space p) holds
( x = 0. ((dim p) -chain-space p) or x = {p} )
set V = (dim p) -chain-space p;
let x be Element of ((dim p) -chain-space p); :: thesis: ( x = 0. ((dim p) -chain-space p) or x = {p} )
x in [#] ((dim p) -chain-space p) ;
then x in {(0. ((dim p) -chain-space p)),{p}} by Th65;
hence ( x = 0. ((dim p) -chain-space p) or x = {p} ) by TARSKI:def 2; :: thesis: verum