We study the provability in subsystems of second-order arithmetic of two theorems of Harrington and Shelah [6] about Borel quasi-orderings of the reals. These theorems turn out to be provable in ATR0, thus giving further evidence to the observation that ATR0 is the minimal subsystem of second-order arithmetic in which significant portion of descriptive set theory can be developed. As in [6] considering the lightface versions of the theorems will be instrumental in their proof and the main techniques employed will (...) be the reflection principles and Gandy forcing. (shrink)