---

Step * of Lemma unit-ss-eq

No Annotations
∀[t,t':{t:ℝ| t ∈ [r0, r1]} ].  uiff(t = t';t ≡ t')
BY
{ (RepUR ``ss-eq ss-sep unit-ss set-ss real-ss mk-ss`` 0 THEN Auto) }

1
1. t : {t:ℝ| (r0 ≤ t) ∧ (t ≤ r1)} 
2. t' : {t:ℝ| (r0 ≤ t) ∧ (t ≤ r1)} 
3. ¬t ≠ t'
⊢ t = t'

---

Latex:

---

Latex:
No  Annotations
\mforall{}[t,t':\{t:\mBbbR{}|  t  \mmember{}  [r0,  r1]\}  ].    uiff(t  =  t';t  \mequiv{}  t')


By

---

Latex:
(RepUR  ``ss-eq  ss-sep  unit-ss  set-ss  real-ss  mk-ss``  0  THEN  Auto)

---

Home Index