---

Step * of Lemma grp_op_polarity

∀[g:OGrp]. ∀[a,b:|g|].  (e ≤ (a * b)) supposing ((e ≤ b) and (e ≤ a))
BY
{ ((RepD) THENA Auto) }

1
1. g : OGrp
2. a : |g|
3. b : |g|
4. e ≤ a
5. e ≤ b
⊢ e ≤ (a * b)

---

Latex:

---

Latex:
\mforall{}[g:OGrp].  \mforall{}[a,b:|g|].    (e  \mleq{}  (a  *  b))  supposing  ((e  \mleq{}  b)  and  (e  \mleq{}  a))


By

---

Latex:
((RepD)  THENA  Auto)

---

Home Index