---

Step * 1 of Lemma oal_le_connex


1. s : LOSet@i'
2. g : OGrp@i'
⊢ Connex(|oal(s;g)|;ps,qs.ps ≤{s,g} qs)
BY
{ % Switch to treating relations-as-1st-class-objects % 
RWH ab_binrelC 0 THEN Try (Fold `xxconnex` 0) }

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

---

Latex:

---

Latex:

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


By

---

Latex:
\%  Switch  to  treating  relations-as-1st-class-objects  \% 
RWH  ab\_binrelC  0  THEN  Try  (Fold  `xxconnex`  0)

---

Home Index