A net in a vector lattice is said to be order convergent to if there is a decreasing net with infimum such that for any there is some such that for all .
The following lemma should exist in the literature, but we are not aware of a reference.
Proof. Suppose that is an order convergent net in to . there is a decreasing net with infimum in such that for any there is some such that for all . Suppose is the infimum of in , then is positive. Since for any , by the definition of order ideal, which follows that is less than the infimum of in . Hence and is order convergent to in .
On the other hand, suppose that is a net in that order converges to in and is dominated by some positive element in . Let be a decreasing net in with infimum such that for any there is some such that for all . Let , then is a decreasing net with infimum in and for all . Hence is order convergent to in . ◻