---

Step * 1 of Lemma oal_lt_char


1. s : LOSet@i'
2. g : OGrp@i'
⊢ (ps,qs:|oal(s;g)|. ps << qs) <≡>{|oal(s;g)|} ((ps,qs:|oal(s;g)|. ps ≤{s,g} qs)\)
BY
{ (((RWW "oal_le_char sp_refl_cl_cancel" 0) THENA Auto) THEN Try (Complete ((BLemma `omon_inc` THEN Auto)))) }

1
1. s : LOSet@i'
2. g : OGrp@i'
⊢ (ps,qs:|oal(s;g)|. ps << qs) <≡>{|oal(s;g)|} (ps,qs:|oal(s;g)|. ps << qs)

2
.....rewrite subgoal..... 
1. s : LOSet@i'
2. g : OGrp@i'
3. (ps,qs:|oal(s;g)|. ps << qs) <≡>{|oal(s;g)|} (ps,qs:|oal(s;g)|. ps << qs)@i
⊢ irrefl(|oal(s;g)|;ps,qs:|oal(s;g)|. ps << qs)

3
.....rewrite subgoal..... 
1. s : LOSet@i'
2. g : OGrp@i'
3. (ps,qs:|oal(s;g)|. ps << qs) <≡>{|oal(s;g)|} (ps,qs:|oal(s;g)|. ps << qs)@i
⊢ st_anti_sym(|oal(s;g)|;ps,qs:|oal(s;g)|. ps << qs)

---

Latex:

---

Latex:

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


By

---

Latex:
(((RWW  "oal\_le\_char  sp\_refl\_cl\_cancel"  0)  THENA  Auto)
  THEN  Try  (Complete  ((BLemma  `omon\_inc`  THEN  Auto)))
  )

---

Home Index