---

Step * 1 1 1 1 of Lemma oal_le_char


1. s : LOSet
2. g : OGrp
3. x : |oal(s;g)|
4. y : |oal(s;g)|
5. g ∈ AbDGrp
6. ↑((x (=b) y) ∨b(x <<b y))
⊢ (x = y ∈ |oal(s;g)|) ∨ (x << y)
BY
{ ((RW bool_to_propC (-1)) THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  s  :  LOSet
2.  g  :  OGrp
3.  x  :  |oal(s;g)|
4.  y  :  |oal(s;g)|
5.  g  \mmember{}  AbDGrp
6.  \muparrow{}((x  (=\msubb{})  y)  \mvee{}\msubb{}(x  <<\msubb{}  y))
\mvdash{}  (x  =  y)  \mvee{}  (x  <<  y)


By

---

Latex:
((RW  bool\_to\_propC  (-1))  THEN  Auto)\mcdot{}

---

Home Index