3. Fremlin proves u > 0 implies x /\ u > 0 > 0 for Archimedean spaces
only. We pick this definition for now.
*) λR:real.λV:archimedean_riesz_space R.λe:V.
3. Fremlin proves u > 0 implies x /\ u > 0 > 0 for Archimedean spaces
only. We pick this definition for now.
*) λR:real.λV:archimedean_riesz_space R.λe:V.