for p being polyhedron
for k being Integer
for m, n being Nat st 1 <= n & n <= num-polytopes (p,k) & 1 <= m & m <= num-polytopes (p,k) & n -th-polytope (p,k) = m -th-polytope (p,k) holds
m = n