---

Step * 1 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 << y)o)
BY
{ (((BLemma `xxconnex_iff_trichot_a`) THENA Auto) THEN Try ((BLemma `omon_inc` THEN Auto))) }

1
1. s : LOSet@i'
2. g : OGrp@i'
⊢ ∀a,b:|oal(s;g)|.  (((x,y:|oal(s;g)|. x << y) a b) ∨ (a = b ∈ |oal(s;g)|) ∨ ((x,y:|oal(s;g)|. x << y) b a))

---

Latex:

---

Latex:

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


By

---

Latex:
(((BLemma  `xxconnex\_iff\_trichot\_a`)  THENA  Auto)  THEN  Try  ((BLemma  `omon\_inc`  THEN  Auto)))

---

Home Index