---

Step * 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 << qs ⇐⇒ ps < qs
BY
{ (((RWW "grp_lt_is_sp_of_leq_a" 0) THENA Auto) THEN Try ((BLemma `ocgrp_abdgrp` THEN Auto))) }

1
1. s : LOSet@i'
2. g : OGrp@i'
3. ps : |oal(s;g)|@i
4. qs : |oal(s;g)|@i
⊢ ps << qs ⇐⇒ (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  <<  qs  \mLeftarrow{}{}\mRightarrow{}  ps  <  qs


By

---

Latex:
(((RWW  "grp\_lt\_is\_sp\_of\_leq\_a"  0)  THENA  Auto)  THEN  Try  ((BLemma  `ocgrp\_abdgrp`  THEN  Auto)))

---

Home Index