I would like to have a list of proofs of the fact that the real line is not meager (also very useful would be a reference to such a list, if it already exists somewhere).
My motivation is the following: in the article Definably complete and Baire structures we defined a first-order notion of Baire structures, and I would like to prove that every definably complete ordered field is definably Baire. To do that, a possible approach would be to take a proof of the fact that $\mathbb R$ is not meager, and adapt it to the first-order situation. The main obstacle to such an adaptation is the fact that we cannot define sets by recursion.