---

Step * of Lemma real-ss-eq

No Annotations
∀[x,y:ℝ].  uiff(x ≡ y;x = y)
BY
{ (RepUR ``real-ss ss-eq ss-sep mk-ss`` 0 THEN EAuto 1) }

---

Latex:

---

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


By

---

Latex:
(RepUR  ``real-ss  ss-eq  ss-sep  mk-ss``  0  THEN  EAuto  1)

---

Home Index