This post originated from my reference request for the definition of an ordered field in constructive mathematics: Proper definition of ordered field in constructive mathematics

We are working in constructive mathematics. For the sake of this post, let us define a ordered field to be a field $K$ with a strict linear order $<$ such that $0 < 1$ and for all elements $a \in K$ and $b \in K$, if $a > 0$ and $b > 0$ then $a + b > 0$ and $a \cdot b > 0$. $K$ has a partial order $\leq$ defined by $a \leq b := \neg(b < a)$. An ordered field is a lattice field if additionally it contains a binary meet function $\min$ and join function $\max$ such that $(K, \leq, \min, \max)$ is a (unbounded) lattice. A nonlattice field is an ordered field where the partial order $\leq$ does not form a lattice.

In one of the comments of my reference request, Geoffrey Irving states

Given a lattice field, one can adjoin a positive transcendental with no other information to get a nonlattice field. And given a nonlattice field, there is a constructive lattice closure that extends it as a constructive field.

Are there proofs of these two statements?