---

Step * of Lemma rleq*_functionality

∀a,b,c,d:ℝ*.  (a = b ⇒ c = d ⇒ (a ≤ c ⇐⇒ b ≤ d))
BY
{ (Auto THEN All (Unfold `rleq*`)) }

1
1. a : ℝ*
2. b : ℝ*
3. c : ℝ*
4. d : ℝ*
5. a = b
6. c = d
7. λa,b. (a ≤ b)*(a,c)
⊢ λa,b. (a ≤ b)*(b,d)

2
1. a : ℝ*
2. b : ℝ*
3. c : ℝ*
4. d : ℝ*
5. a = b
6. c = d
7. λa,b. (a ≤ b)*(b,d)
⊢ λa,b. (a ≤ b)*(a,c)

---

Latex:

---

Latex:
\mforall{}a,b,c,d:\mBbbR{}*.    (a  =  b  {}\mRightarrow{}  c  =  d  {}\mRightarrow{}  (a  \mleq{}  c  \mLeftarrow{}{}\mRightarrow{}  b  \mleq{}  d))


By

---

Latex:
(Auto  THEN  All  (Unfold  `rleq*`))

---

Home Index