---

Step * 1 1 1 1 of Lemma oal_lt_iff_grp_lt


1. s : LOSet@i'
2. g : OGrp@i'
3. ps : |oal(s;g)|@i
4. qs : |oal(s;g)|@i
⊢ ps [(x,y:|oal(s;g)|. x ≤{s,g} y)\] qs ⇐⇒ (ps ≤ qs) ∧ (¬(qs ≤ ps))
BY
{ Force `5` (Eval ``binrel_ap s_part`` 0) }

1
1. s : LOSet@i'
2. g : OGrp@i'
3. ps : |oal(s;g)|@i
4. qs : |oal(s;g)|@i
⊢ (ps ≤{s,g} qs) ∧ (¬(qs ≤{s,g} ps)) ⇐⇒ (ps ≤ qs) ∧ (¬(qs ≤ ps))

---

Latex:

---

Latex:

1.  s  :  LOSet@i'
2.  g  :  OGrp@i'
3.  ps  :  |oal(s;g)|@i
4.  qs  :  |oal(s;g)|@i
\mvdash{}  ps  [(x,y:|oal(s;g)|.  x  \mleq{}\{s,g\}  y)\mbackslash{}]  qs  \mLeftarrow{}{}\mRightarrow{}  (ps  \mleq{}  qs)  \mwedge{}  (\mneg{}(qs  \mleq{}  ps))


By

---

Latex:
Force  `5`  (Eval  ``binrel\_ap  s\_part``  0)

---

Home Index