loop in simplicial complex



Dear all,

I need a reference for the lemma below.

Let X be a simplicial complex with a fixed vertex x_0.

A combinatorial loop in X is a sequence (x_0,x_1,...,x_n=x_0) of vertices
such that {x_i,x_{i+1}) is an edge for all i.

Consider the equivalence relation, called "combinatorially homotopic",
between combinatorial loops, generated by the following "elementary
steps":

- (x_0,...,x_n) ~ (x_0,...,x_i,y,x_{i+1},...,x_n)
- (x_0,...,x_n) ~ (x_0,...,x_{i-1},x_{i+1},...,x_n) whenever
{x_{i-1},x_i,x_{i+1}} is a 2-simplex.

On the other hand, a combinatorial defines a loop in the topological space
X_top, well-defined up to homotopy.

Lemma: if a combinatorial loop is homotopically trivial in pi_1(X_top),
then it is combinatorially homotopic to the trivial loop.

It seems that this lemma is well-known and widely used, but I did not find
a precise reference. Does someone have one?

Thanks in advance,

--
Yves
.