---

Step * 1 of Lemma rat-point-in-face


1. C1 : ℚ
2. C2 : ℚ
3. D1 : ℚ
4. D2 : ℚ
5. a : ℚ
⊢ (((fst(<D1, D2>)) ≤ a) ∧ (a ≤ (snd(<D1, D2>)))) ⇒ (↑Inhabited(<C1, C2>)) ⇒ <D1, D2> ≤ <C1, C2> ⇒ (((fst(<C1, C2>)) \000C≤ a) ∧ (a ≤ (snd(<C1, C2>))))
BY
{ (RepUR ``inhabited-rat-interval rat-interval-face rat-point-interval`` 0
   THEN (RW assert_pushdownC 0 THENA Auto)
   THEN RepeatFor 3 ((D 0 THENA Auto))
   THEN SplitOrHyps
   THEN (EqHD (-1) THENA Auto)
   THEN All Reduce
   THEN Auto) }

---

Latex:

---

Latex:

1.  C1  :  \mBbbQ{}
2.  C2  :  \mBbbQ{}
3.  D1  :  \mBbbQ{}
4.  D2  :  \mBbbQ{}
5.  a  :  \mBbbQ{}
\mvdash{}  (((fst(<D1,  D2>))  \mleq{}  a)  \mwedge{}  (a  \mleq{}  (snd(<D1,  D2>))))  {}\mRightarrow{}  (\muparrow{}Inhabited(<C1,  C2>))  {}\mRightarrow{}  <D1,  D2>  \mleq{}  <C1,  C2>  {}\000C\mRightarrow{}  (((fst(<C1,  C2>))  \mleq{}  a)  \mwedge{}  (a  \mleq{}  (snd(<C1,  C2>))))


By

---

Latex:
(RepUR  ``inhabited-rat-interval  rat-interval-face  rat-point-interval``  0
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  RepeatFor  3  ((D  0  THENA  Auto))
  THEN  SplitOrHyps
  THEN  (EqHD  (-1)  THENA  Auto)
  THEN  All  Reduce
  THEN  Auto)

---

Home Index