---

Step * of Lemma trivial_sym_grp

∀p:Sym(1). (p = id_perm() ∈ Sym(1))
BY
{ (D 0 THENA Auto) }

1
1. p : Sym(1)
⊢ p = id_perm() ∈ Sym(1)

---

Latex:

---

Latex:
\mforall{}p:Sym(1).  (p  =  id\_perm())


By

---

Latex:
(D  0  THENA  Auto)

---

Home Index