We show that an LK proof of size $m$ of a monotone sequent (a sequent

that contains only formulas in the basis $\wedge,\vee$) can be turned

into a proof containing only monotone formulas of size $m^{O(\log m)}$

and with the number of proof lines polynomial in $m$. Also we show

that some interesting special cases, namely the functional and the

onto versions of PHP and a version of the Matching Principle, have

polynomial size monotone proofs.