---

Step * 1 of Lemma set_lt_is_sp_of_leq


1. p : PosetSig
2. a : |p|
3. b : |p|
⊢ uiff(a <p b;strict_part(x,y.x ≤ y;a;b))
BY
{ RepUnfolds ``strict_part set_lt set_blt`` 0 }

1
1. p : PosetSig
2. a : |p|
3. b : |p|
⊢ uiff(↑((a (≤b) b) ∧b (¬b(b (≤b) a)));(a ≤ b) ∧ (¬(b ≤ a)))

---

Latex:

---

Latex:

1.  p  :  PosetSig
2.  a  :  |p|
3.  b  :  |p|
\mvdash{}  uiff(a  <p  b;strict\_part(x,y.x  \mleq{}  y;a;b))


By

---

Latex:
RepUnfolds  ``strict\_part  set\_lt  set\_blt``  0

---

Home Index