The real dominated-extension principle as an additional hypothesis over ZF

Work over ZF. The real dominated-extension principle, denoted HB, is the following assertion:

For every real vector space $X$, every sublinear functional $p:X\to \mathbb{R}$ in the sense of A sublinear functional on a real vector space, every real linear subspace $M\le X$ in the sense of Linear subspace of a vector space, and every real linear functional $g:M\to \mathbb{R}$ in the sense of Linear functionals and the algebraic dual $V^{\ast }=\mathcal{L}(V,F)$, $(\mathrm{\forall }m\in M,g(m)\le p(m))⟹\mathrm{\exists }F:X\to \mathbb{R}(F\text{ is real linear},F{\mathrm{\mid }}_M=g,\mathrm{\forall }x\in X,F(x)\le p(x))\mathrm{.}$

This names an additional principle; it does not assert a proof of HB in ZF. Subsequent results explicitly state when they assume HB. Neither topology nor completeness is part of this assertion. The subspace may be $\{0\}$ or all of $X$. Sublinearity at scalar zero gives $p(0)=0$, and a linear functional has value zero at zero.

Brezis Theorem 1.1, p.1 (assertion only); Teschl Theorem 4.13, pp.112–113 (sublinear special case).