---

Step * 1 of Lemma qmin-symmetry

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

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

---

Latex:

---

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


By

---

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

---

Home Index