---

Step * of Lemma fset-union-empty

∀[eq,s:Top].  (s ⋃ {} ~ s)
BY
{ ((Auto THEN RepUR ``fset-union l-union empty-fset`` 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[eq,s:Top].    (s  \mcup{}  \{\}  \msim{}  s)


By

---

Latex:
((Auto  THEN  RepUR  ``fset-union  l-union  empty-fset``  0)  THEN  Auto)

---

Home Index