Least fixed point logic is efficiently $\operatorname{P}$-bounded for $\operatorname{P} \Leftrightarrow L_\leq$ is a logic for $\operatorname{P}$

Question

A least-fixed point (LFP) formula is $\leq m$-invariant iff f.a. structrues $\mathcal{A}$ with $|A| \leq m$ and all orderings $<_1,<_2$ on $A$

$$(\mathcal{A},<_1) \models_{LFP} \varphi \Leftrightarrow (\mathcal{A},<_1) \models_{LFP} \varphi.$$

The logic $L_\leq$ is defined such that the modelling-relation is

$$ \mathcal{A} \models_{L_\leq} \varphi \Leftrightarrow \varphi \textrm{ is $\leq m$-invariant and } (\mathcal{A},<)\models_{LFP}\varphi \textrm{ for some} <.$$

A logic $L$ is efficiently $\operatorname{P}$-bounded for $\operatorname{P}$ if

• for each $Q \in \operatorname{P}$ there is a $\varphi \in L$ which axiomatizes $Q$
• for each $\varphi \in L$ there is polynomial $p$ such that the modelling relation $\mathcal{A} \models_L \varphi$ can be decided by an algorithm in $\leq p(\|\mathcal{A}\|)$ steps

A known result is that LFP is an efficiently $\operatorname{P}$-bound logic for $\operatorname{P}$ on the class of ordered structures. A paper states that one can easily deduce from the result that $L_\leq$ is a logic for $\operatorname{P}$. Any ideas how?