---

Step * 1 3 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
⊢ st_anti_sym(|oal(s;g)|;ps,qs:|oal(s;g)|. ps << qs)
BY
{ (((BLemma `irrefl_trans_imp_sasym` 
   THENM Force `5` (Eval ``xxirrefl xxtrans`` 0) 
   THENM Backchain ``oal_lt_irrefl oal_lt_trans`` ) THENA Auto)
   THEN BLemma `ocgrp_abdgrp`
   THEN 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{}  st\_anti\_sym(|oal(s;g)|;ps,qs:|oal(s;g)|.  ps  <<  qs)


By

---

Latex:
(((BLemma  `irrefl\_trans\_imp\_sasym` 
  THENM  Force  `5`  (Eval  ``xxirrefl  xxtrans``  0) 
  THENM  Backchain  ``oal\_lt\_irrefl  oal\_lt\_trans``  )  THENA  Auto)
  THEN  BLemma  `ocgrp\_abdgrp`
  THEN  Auto)

---

Home Index