---

Step * 1 of Lemma common-face-inhabited-intersection


1. v7 : ℚ
2. v8 : ℚ
3. v5 : ℚ
4. v6 : ℚ
5. v3 : ℚ
6. v4 : ℚ
7. v3 ≤ v4
8. v5 ≤ v6
9. (<v7, v8> = <v5, v5> ∈ ℚInterval) ∨ (<v7, v8> = <v6, v6> ∈ ℚInterval) ∨ (<v7, v8> = <v5, v6> ∈ ℚInterval)
10. (<v7, v8> = <v3, v3> ∈ ℚInterval) ∨ (<v7, v8> = <v4, v4> ∈ ℚInterval) ∨ (<v7, v8> = <v3, v4> ∈ ℚInterval)
⊢ qmax(v5;v3) ≤ qmin(v6;v4)
BY
{ (SplitOrHyps
   THEN ∀h:hyp. (EqHD h THENA Auto) 
   THEN All Reduce
   THEN (RWO "qmax_lb" 0 THENA Auto)
   THEN RWO "qmin_ub" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  v7  :  \mBbbQ{}
2.  v8  :  \mBbbQ{}
3.  v5  :  \mBbbQ{}
4.  v6  :  \mBbbQ{}
5.  v3  :  \mBbbQ{}
6.  v4  :  \mBbbQ{}
7.  v3  \mleq{}  v4
8.  v5  \mleq{}  v6
9.  (<v7,  v8>  =  <v5,  v5>)  \mvee{}  (<v7,  v8>  =  <v6,  v6>)  \mvee{}  (<v7,  v8>  =  <v5,  v6>)
10.  (<v7,  v8>  =  <v3,  v3>)  \mvee{}  (<v7,  v8>  =  <v4,  v4>)  \mvee{}  (<v7,  v8>  =  <v3,  v4>)
\mvdash{}  qmax(v5;v3)  \mleq{}  qmin(v6;v4)


By

---

Latex:
(SplitOrHyps
  THEN  \mforall{}h:hyp.  (EqHD  h  THENA  Auto) 
  THEN  All  Reduce
  THEN  (RWO  "qmax\_lb"  0  THENA  Auto)
  THEN  RWO  "qmin\_ub"  0
  THEN  Auto)

---

Home Index