---

Step * of Lemma q-between-overlap

∀a,b,c,d,q:ℚ.
  (∃x,y:ℚ. (x < q < y ∧ (∀q':ℚ. a < q' < b ∧ c < q' < d supposing x < q' < y))) supposing (c < q < d and a < q < b)
BY
{ (Auto
   THEN InstConcl [⌜qmax(a;c)⌝;⌜qmin(b;d)⌝]⋅
   THEN Auto
   THEN All
   (RepUR ``q-between``)⋅
   THEN Auto
   THEN All (\h. RWO "qmax_strict_lb qmin_strict_ub" h )⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}a,b,c,d,q:\mBbbQ{}.
    (\mexists{}x,y:\mBbbQ{}.  (x  <  q  <  y  \mwedge{}  (\mforall{}q':\mBbbQ{}.  a  <  q'  <  b  \mwedge{}  c  <  q'  <  d  supposing  x  <  q'  <  y)))  supposing 
          (c  <  q  <  d  and 
          a  <  q  <  b)


By

---

Latex:
(Auto
  THEN  InstConcl  [\mkleeneopen{}qmax(a;c)\mkleeneclose{};\mkleeneopen{}qmin(b;d)\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  All
  (RepUR  ``q-between``)\mcdot{}
  THEN  Auto
  THEN  All  (\mbackslash{}h.  RWO  "qmax\_strict\_lb  qmin\_strict\_ub"  h  )\mcdot{}
  THEN  Auto)

---

Home Index