---

Step * 1 of Lemma oal_le_is_order


1. s : LOSet@i'
2. g : OGrp@i'
⊢ Order(|oal(s;g)|;ps,qs.ps ≤{s,g} qs)
BY
{ (% Switch to treating relations-as-1st-class-objects % 
   ((RWH ab_binrelC 0  
   THENM RWW "xxorder_eq_order<" 0) THENA Auto)
   THEN Try ((BLemma `omon_inc` THEN Complete (Auto)))
   THEN Try ((BLemma `ocgrp_abdgrp` THEN Complete (Auto)))) }

1
1. s : LOSet@i'
2. g : OGrp@i'
⊢ order(|oal(s;g)|;x,y:|oal(s;g)|. x ≤{s,g} y)

---

Latex:

---

Latex:

1.  s  :  LOSet@i'
2.  g  :  OGrp@i'
\mvdash{}  Order(|oal(s;g)|;ps,qs.ps  \mleq{}\{s,g\}  qs)


By

---

Latex:
(\%  Switch  to  treating  relations-as-1st-class-objects  \% 
  ((RWH  ab\_binrelC  0   
  THENM  RWW  "xxorder\_eq\_order<"  0)  THENA  Auto)
  THEN  Try  ((BLemma  `omon\_inc`  THEN  Complete  (Auto)))
  THEN  Try  ((BLemma  `ocgrp\_abdgrp`  THEN  Complete  (Auto))))

---

Home Index