---

Step * 1 1 of Lemma oal_le_connex


1. s : LOSet@i'
2. g : OGrp@i'
⊢ connex(|oal(s;g)|;x,y:|oal(s;g)|. x ≤{s,g} y)
BY
{ (((RWW "oal_le_char" 0) THENA Auto) THEN Try ((BLemma `ocgrp_abdgrp` THEN Auto))) }

1
1. s : LOSet@i'
2. g : OGrp@i'
⊢ connex(|oal(s;g)|;(x,y:|oal(s;g)|. x << y)o)

---

Latex:

---

Latex:

1.  s  :  LOSet@i'
2.  g  :  OGrp@i'
\mvdash{}  connex(|oal(s;g)|;x,y:|oal(s;g)|.  x  \mleq{}\{s,g\}  y)


By

---

Latex:
(((RWW  "oal\_le\_char"  0)  THENA  Auto)  THEN  Try  ((BLemma  `ocgrp\_abdgrp`  THEN  Auto)))

---

Home Index