---

Step * 1 1 1 1 1 1 1 1 of Lemma real-fun-implies-sfun-general


1. z : ℝ
2. a : ℝ
3. b : ℝ
4. a ≤ b
⊢ rmin(b;rmax(a;z)) ∈ {z:ℝ| (a ≤ z) ∧ (z ≤ b)} 
BY
{ (MemTypeCD THEN EAuto 2) }

---

Latex:

---

Latex:

1.  z  :  \mBbbR{}
2.  a  :  \mBbbR{}
3.  b  :  \mBbbR{}
4.  a  \mleq{}  b
\mvdash{}  rmin(b;rmax(a;z))  \mmember{}  \{z:\mBbbR{}|  (a  \mleq{}  z)  \mwedge{}  (z  \mleq{}  b)\} 


By

---

Latex:
(MemTypeCD  THEN  EAuto  2)

---

Home Index