---

Step * of Lemma partition-refines_weakening

∀I:Interval. ∀P,Q:partition(I).  ((P = Q ∈ partition(I)) ⇒ P refines Q) supposing icompact(I)
BY
{ (Auto THEN HypSubst (-1) 0 THEN Auto) }

1
1. I : Interval
2. [%] : icompact(I)
3. P : partition(I)
4. Q : partition(I)
5. P = Q ∈ partition(I)
⊢ Q refines Q

---

Latex:

---

Latex:
\mforall{}I:Interval.  \mforall{}P,Q:partition(I).    ((P  =  Q)  {}\mRightarrow{}  P  refines  Q)  supposing  icompact(I)


By

---

Latex:
(Auto  THEN  HypSubst  (-1)  0  THEN  Auto)

---

Home Index