---

Step * of Lemma rmetric-meq

∀[x,y:ℝ].  uiff(x ≡ y;x = y)
BY
{ (RepUR ``meq rmetric`` 0 THEN EAuto 1) }

1
1. x : ℝ
2. y : ℝ
3. x = y
⊢ |x - y| = r0

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].    uiff(x  \mequiv{}  y;x  =  y)


By

---

Latex:
(RepUR  ``meq  rmetric``  0  THEN  EAuto  1)

---

Home Index