---

Step * 1 of Lemma oal_le_char


1. s : LOSet
2. g : OGrp
3. x : |oal(s;g)|
4. y : |oal(s;g)|
⊢ (ps,qs:|oal(s;g)|. ps ≤{s,g} qs) x y ⇐⇒ ((ps,qs:|oal(s;g)|. ps << qs)o) x y
BY
{ Force `5` (Eval ``refl_cl`` 0) }

1
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)

---

Latex:

---

Latex:

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


By

---

Latex:
Force  `5`  (Eval  ``refl\_cl``  0)

---

Home Index