---

Step * of Lemma rless*_functionality

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

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  <  c  \mLeftarrow{}{}\mRightarrow{}  b  <  d))


By

---

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

---

Home Index