---

Step * 2 of Lemma equipollent-product-one


1. ℕ1 ~ Top
⊢ ∀[A:Type]. (A × ℕ1 ~ A ∧ ℕ1 × A ~ A)
BY
{ (Intro THEN (RWW "1 equipollent-identity-left equipollent-identity-right" 0 THEN Auto) THEN RelRST THEN Auto) }

---

Latex:

---

Latex:

1.  \mBbbN{}1  \msim{}  Top
\mvdash{}  \mforall{}[A:Type].  (A  \mtimes{}  \mBbbN{}1  \msim{}  A  \mwedge{}  \mBbbN{}1  \mtimes{}  A  \msim{}  A)


By

---

Latex:
(Intro
  THEN  (RWW  "1  equipollent-identity-left  equipollent-identity-right"  0  THEN  Auto)
  THEN  RelRST
  THEN  Auto)

---

Home Index