An infinitary characterisation of the first-order sentences true in all substructures of a structure $\mathbf{M}$ is used to obtain partial reduction of the decision problem for such sentences to that for $\mathrm{Th}(\mathbf{M})$. For the relational structure $\langle\mathbf{R}, \leq, +\rangle$ this gives a decision procedure for the $\exists x\forall y$-part of the theory of all substructures, yet we show that the $\exists x_1x_2\forall y$-part, and the entire theory, is $\Pi^1_1$-complete. The theory of all ordered subsemigroups of $\langle\mathbf{R}, \leq, +\rangle$ is also shown $\Pi^1_1$-complete. Applications in the philosophy of science are mentioned.