---

Step * 1 1 of Lemma oal_le_char


1. s : LOSet
2. g : OGrp
3. x : |oal(s;g)|
4. y : |oal(s;g)|
⊢ x ≤{s,g} y ⇐⇒ (x = y ∈ |oal(s;g)|) ∨ (x << y)
BY
{ RepUnfolds ``oal_le oal_ble`` 0 }

1
1. s : LOSet
2. g : OGrp
3. x : |oal(s;g)|
4. y : |oal(s;g)|
⊢ ↑((x (=b) y) ∨b(x <<b y)) ⇐⇒ (x = y ∈ |oal(s;g)|) ∨ (x << y)

---

Latex:

---

Latex:

1.  s  :  LOSet
2.  g  :  OGrp
3.  x  :  |oal(s;g)|
4.  y  :  |oal(s;g)|
\mvdash{}  x  \mleq{}\{s,g\}  y  \mLeftarrow{}{}\mRightarrow{}  (x  =  y)  \mvee{}  (x  <<  y)


By

---

Latex:
RepUnfolds  ``oal\_le  oal\_ble``  0

---

Home Index