Theorem 2
Tag 0AYD, permanent. Cite it as [Bourbaki, Tag 0AYD].
Lie Groups and Lie Algebras, chapter VI, § 4. Classification of root systems
The Coxeter groups defined by the Coxeter graphs A_l, B_l, ..., I_2(p) of Th. 1 are finite.
This is clear for I_2(p), the corresponding group being the dihedral group of order 2p (Chap. IV, § 1, no. 9). For H_4 the corresponding quadratic form is
Since is , this form is positive non-degenerate, and the corresponding Coxeter group is finite. The same holds for that corresponding to , since it is isomorphic to a subgroup of the preceding (Chap. IV, § 1, no. 8).
For the types , we shall construct, in Nos. 5 to 13, root systems having the corresponding groups as Weyl groups. We shall see that these groups are not only finite, but crystallographic (§ 2, no. 5).
Bourbaki puts the proof directly after the statement, so what is above is the statement and its proof together.