Theorem 2

The pair $(W, S)$ is a Coxeter system. Moreover, for $s \in S$ and $w \in W$, the relations $C(sw) = C(s).C(w)$ and $l_S(sw) > l_S(w)$ are equivalent.

For any $s \in S$, let $P_s$ be the set of elements $w \in W$ such that

We are going to verify that the $P_s$ satisfy conditions (A'), (B') and (C) of § 1, no. 7; the two assertions of the theorem will then follow from Prop. 6 of § 1, no. 7.

Condition (A') is clear.

We verify (B'). If $P_s$ and $sP_s$ had an element $w$ in common, we would have $w \in P_s$ and $sw \in P_s$, and hence

It would follow that $C(s).C(s).C(w) = C(w)$ and, by formula (5), this would imply that $C(w) = C(sw)$, which would contradict Th. 1.

We verify (C). Let $s, s' \in S$ and $w, w' \in W$ with $w' = ws'$. The assumption that $w \in P_s$ and $w' \notin P_s$ implies that

by (3).

From (9) and the relation $w = w's'$, it follows that

By formula (2'), $C(w').C(s') \subset C(w') \cup C(w's')$, which immediately implies that Since $C(w')$ is a union of left cosets $gB$ and since formula (10) shows that $C(s)w'$ meets $C(w')$ and a fortiori that $C(s)w's'B$ meets $C(w')s'B$. It follows from formulas (11) and (12) that the double coset $C(sw)$ is equal to one of the double cosets $C(ws')$ and $C(w)$; since $sw \neq w$, Th. 1 allows us to conclude that $sw = ws'$.