---

Step * 1 1 1 of Lemma hgrp_of_ocgrp_wf2


1. g : OGrp
2. ∀[a1,a2:|g|+].  ((a1 * a2) = (a1 * a2) ∈ |g|)
3. e = e ∈ |g|
4. a1 : |g|+@i
5. a2 : |g|+@i
6. a1 = a2 ∈ |g|@i
⊢ a1 = a2 ∈ |g|+
BY
{ (EqTypeCD THEN Auto) }

1
.....set predicate..... 
1. g : OGrp
2. ∀[a1,a2:|g|+].  ((a1 * a2) = (a1 * a2) ∈ |g|)
3. e = e ∈ |g|
4. a1 : |g|+@i
5. a2 : |g|+@i
6. a1 = a2 ∈ |g|@i
⊢ e ≤ a1

---

Latex:

---

Latex:

1.  g  :  OGrp
2.  \mforall{}[a1,a2:|g|\msupplus{}].    ((a1  *  a2)  =  (a1  *  a2))
3.  e  =  e
4.  a1  :  |g|\msupplus{}@i
5.  a2  :  |g|\msupplus{}@i
6.  a1  =  a2@i
\mvdash{}  a1  =  a2


By

---

Latex:
(EqTypeCD  THEN  Auto)

---

Home Index