MSO logic of the real order with the set quantifiers ranging over the Borel sets

A celebrated 1969 theorem of Michael Rabin is that the monadic second-order (MSO) theory of the real order where the monadic quantifier is allowed only to range over the closed or $F_\sigma$-sets, is decidable. In 1975 Saharon Shelah conjectured that if the monadic quantifier is allowed to range over the Borel subsets of the reals, the resulting MSO theory is still decidable. We confirm this conjecture. In fact, the conjecture can be understood in the weak form, in the language where there is a special symbol for each level of the Borel hierarchy, or in a strong form where the language simply has a symbol for Borel sets. We confirm both versions of the conjecture, the former one by interpreting it in $\mathrm{S2S}$ and the latter one by in addition using Büchi's theorem that $\mathrm{MSO} \left( \omega_1, \lt \right)$ is decidable.