---

Step * 1 1 of Lemma set_leq_iff_lt_or_eq


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|)
BY
{ (((AddAllProperties 1) THENA Auto) THEN Reduce 0 THEN Auto) }

1
1. s : POSet{i}@i'
2. IsEqFun(|s|;=b)
3. UniformPreorder(|s|;a,b.a ≤ b)
4. UniformlyAntiSym(|s|;a,b.a ≤ b)
5. a : |s|@i
6. b : |s|@i
7. a ≤ b@i
⊢ (a <s b) ∨ (a = b ∈ |s|)

2
1. s : POSet{i}@i'
2. IsEqFun(|s|;=b)
3. UniformPreorder(|s|;a,b.a ≤ b)
4. UniformlyAntiSym(|s|;a,b.a ≤ b)
5. a : |s|@i
6. b : |s|@i
7. (a <s b) ∨ (a = b ∈ |s|)@i
⊢ a ≤ b

---

Latex:

---

Latex:

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


By

---

Latex:
(((AddAllProperties  1)  THENA  Auto)  THEN  Reduce  0  THEN  Auto)

---

Home Index