---

Step * 1 of Lemma qless-witness


1. a : ℚ
2. b : ℚ
3. a < b
⊢ ⋅ ∈ a < b
BY
{ Assert ⌜TERMOF{decidable__qless:o, 1:l} a b ∈ Dec(a < b)⌝⋅ }

1
.....assertion..... 
1. a : ℚ
2. b : ℚ
3. a < b
⊢ TERMOF{decidable__qless:o, 1:l} a b ∈ Dec(a < b)

2
1. a : ℚ
2. b : ℚ
3. a < b
4. TERMOF{decidable__qless:o, 1:l} a b ∈ Dec(a < b)
⊢ ⋅ ∈ a < b

---

Latex:

---

Latex:

1.  a  :  \mBbbQ{}
2.  b  :  \mBbbQ{}
3.  a  <  b
\mvdash{}  \mcdot{}  \mmember{}  a  <  b


By

---

Latex:
Assert  \mkleeneopen{}TERMOF\{decidable\_\_qless:o,  1:l\}  a  b  \mmember{}  Dec(a  <  b)\mkleeneclose{}\mcdot{}

---

Home Index