---

Step * 1 2 of Lemma oal_lt_char

.....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)
BY
{ ((Force `5` (Eval ``xxirrefl`` 0) 
THENM BLemma `oal_lt_irrefl`) THENA Auto) }

---

Latex:

---

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


By

---

Latex:
((Force  `5`  (Eval  ``xxirrefl``  0) 
THENM  BLemma  `oal\_lt\_irrefl`)  THENA  Auto)

---

Home Index