---

Step * of Lemma oal_neg_right_inv

∀a:LOSet. ∀b:AbDGrp. ∀ps:|oal(a;b)|.  ((ps ++ (--ps)) = 00 ∈ |oal(a;b)|)
BY
{ ((RepD THENM RWH (LemmaC `oal_merge_comm`) 0 
THENM BLemma `oal_neg_left_inv`) THENA Auto) }

---

Latex:

---

Latex:
\mforall{}a:LOSet.  \mforall{}b:AbDGrp.  \mforall{}ps:|oal(a;b)|.    ((ps  ++  (--ps))  =  00)


By

---

Latex:
((RepD  THENM  RWH  (LemmaC  `oal\_merge\_comm`)  0 
THENM  BLemma  `oal\_neg\_left\_inv`)  THENA  Auto)

---

Home Index