---

Step * of Lemma set_lt_is_sp_of_leq

∀[p:PosetSig]. ∀[a,b:|p|].  uiff(a <p b;strict_part(x,y.x ≤ y;a;b))
BY
{ ((RepD) THENA Auto) }

1
1. p : PosetSig
2. a : |p|
3. b : |p|
⊢ uiff(a <p b;strict_part(x,y.x ≤ y;a;b))

---

Latex:

---

Latex:
\mforall{}[p:PosetSig].  \mforall{}[a,b:|p|].    uiff(a  <p  b;strict\_part(x,y.x  \mleq{}  y;a;b))


By

---

Latex:
((RepD)  THENA  Auto)

---

Home Index