---

Step * 1 of Lemma set_leq_iff_lt_or_eq


1. s : POSet{i}@i'
2. a : |s|@i
3. b : |s|@i
⊢ a ≤ b ⇐⇒ (a <s b) ∨ (a = b ∈ |s|)
BY
{ % Need 2, since iff is first! % 
RWN 2 ab_binrelC 0 }

1
1. s : POSet{i}@i'
2. a : |s|@i
3. b : |s|@i
⊢ (x,y:|s|. x ≤ y) a b ⇐⇒ (a <s b) ∨ (a = b ∈ |s|)

---

Latex:

---

Latex:

1.  s  :  POSet\{i\}@i'
2.  a  :  |s|@i
3.  b  :  |s|@i
\mvdash{}  a  \mleq{}  b  \mLeftarrow{}{}\mRightarrow{}  (a  <s  b)  \mvee{}  (a  =  b)


By

---

Latex:
\%  Need  2,  since  iff  is  first!  \% 
RWN  2  ab\_binrelC  0

---

Home Index