---

Step * 1 of Lemma qmax-symmetry

.....falsecase..... 
1. x : ℚ
2. y : ℚ
3. ¬(x ≤ y)
4. ¬(y ≤ x)
⊢ x = y ∈ ℚ
BY
{ xxx((RWO "qle_complement_qorder" 3 THENA Auto) THEN (RWO "qle_complement_qorder" 4 THENA Auto))xxx }

1
1. x : ℚ
2. y : ℚ
3. y < x
4. x < y
⊢ x = y ∈ ℚ

---

Latex:

---

Latex:
.....falsecase..... 
1.  x  :  \mBbbQ{}
2.  y  :  \mBbbQ{}
3.  \mneg{}(x  \mleq{}  y)
4.  \mneg{}(y  \mleq{}  x)
\mvdash{}  x  =  y


By

---

Latex:
xxx((RWO  "qle\_complement\_qorder"  3  THENA  Auto)  THEN  (RWO  "qle\_complement\_qorder"  4  THENA  Auto))xxx

---

Home Index