---

Step * of Lemma sq_stable__icompact

∀I:Interval. SqStable(icompact(I))
BY
{ (Auto
   THEN D 1
   THEN DProdsAndUnions
   THEN RepUR ``icompact i-closed i-finite i-nonvoid i-member`` 0
   THEN D 0
   THEN Auto
   THEN Try (Complete ((Assert ⌜False⌝⋅ THEN Auto)))) }

1
1. x : ℝ@i
2. x2 : ℝ@i
3. ↓(∃r:ℝ. ((x ≤ r) ∧ (r ≤ x2))) ∧ (True ∧ True) ∧ True ∧ True@i
⊢ ∃r:ℝ. ((x ≤ r) ∧ (r ≤ x2))

---

Latex:

---

Latex:
\mforall{}I:Interval.  SqStable(icompact(I))


By

---

Latex:
(Auto
  THEN  D  1
  THEN  DProdsAndUnions
  THEN  RepUR  ``icompact  i-closed  i-finite  i-nonvoid  i-member``  0
  THEN  D  0
  THEN  Auto
  THEN  Try  (Complete  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto))))

---

Home Index