---

Step * of Lemma iproper-nonvoid

∀I:Interval. (iproper(I) ⇒ i-nonvoid(I))
BY
{ (Auto
   THEN D 1
   THEN D 2
   THEN D 1
   THEN All (RepUR ``iproper i-nonvoid i-finite left-endpoint right-endpoint``)
   THEN All (RepUR ``i-member endpoints``)
   THEN ((DVar `x' THEN Reduce 0) ORELSE (D 0 With ⌜r0⌝  THEN Auto))) }

1
1. x1 : ℝ + ℝ
2. x2 : ℝ
3. (True ∧ True) ⇒ (case x1 of inl(a) => a | inr(a) => a < case inl x2 of inl(b) => b | inr(b) => b)
⊢ ∃r:ℝ. case x1 of inl(a) => (a ≤ r) ∧ (r ≤ x2) | inr(a) => (a < r) ∧ (r ≤ x2)

2
1. x1 : ℝ + ℝ
2. y : ℝ
3. (True ∧ True) ⇒ (case x1 of inl(a) => a | inr(a) => a < case inr y  of inl(b) => b | inr(b) => b)
⊢ ∃r:ℝ. case x1 of inl(a) => (a ≤ r) ∧ (r < y) | inr(a) => (a < r) ∧ (r < y)

3
1. y : Top
2. x1 : ℝ
3. (False ∧ True) ⇒ (case ⊥ of inl(a) => a | inr(a) => a < case inl x1 of inl(b) => b | inr(b) => b)
⊢ ∃r:ℝ. (r ≤ x1)

4
1. y : Top
2. y1 : ℝ
3. (False ∧ True) ⇒ (case ⊥ of inl(a) => a | inr(a) => a < case inr y1  of inl(b) => b | inr(b) => b)
⊢ ∃r:ℝ. (r < y1)

5
1. x1 : ℝ
2. y : Top
3. (True ∧ False) ⇒ (case inl x1 of inl(a) => a | inr(a) => a < case ⊥ of inl(b) => b | inr(b) => b)
⊢ ∃r:ℝ. (x1 ≤ r)

6
1. y1 : ℝ
2. y : Top
3. (True ∧ False) ⇒ (case inr y1  of inl(a) => a | inr(a) => a < case ⊥ of inl(b) => b | inr(b) => b)
⊢ ∃r:ℝ. (y1 < r)

---

Latex:

---

Latex:
\mforall{}I:Interval.  (iproper(I)  {}\mRightarrow{}  i-nonvoid(I))


By

---

Latex:
(Auto
  THEN  D  1
  THEN  D  2
  THEN  D  1
  THEN  All  (RepUR  ``iproper  i-nonvoid  i-finite  left-endpoint  right-endpoint``)
  THEN  All  (RepUR  ``i-member  endpoints``)
  THEN  ((DVar  `x'  THEN  Reduce  0)  ORELSE  (D  0  With  \mkleeneopen{}r0\mkleeneclose{}    THEN  Auto)))

---

Home Index