---

Step * 1 1 of Lemma oal_merge_preserves_le


1. s : LOSet@i'
2. g : OGrp@i'
3. ps : |oal(s;g)|@i
4. qs : |oal(s;g)|@i
5. rs : |oal(s;g)|@i
6. qs ≤ rs@1
⊢ (ps * qs) ≤ (ps * rs)
BY
{ ((BLemma `grp_op_preserves_le`) THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  LOSet@i'
2.  g  :  OGrp@i'
3.  ps  :  |oal(s;g)|@i
4.  qs  :  |oal(s;g)|@i
5.  rs  :  |oal(s;g)|@i
6.  qs  \mleq{}  rs@1
\mvdash{}  (ps  *  qs)  \mleq{}  (ps  *  rs)


By

---

Latex:
((BLemma  `grp\_op\_preserves\_le`)  THEN  Auto)

---

Home Index