for p being polyhedron holds ((dim p) -boundary p) . {p} = ((dim p) - 1) -polytopes p