---

Step * of Lemma set_lt_is_sp_of_leq_a

∀[p:PosetSig]. ∀[a,b:|p|].  uiff(a <p b;(a ≤ b) ∧ (¬(b ≤ a)))
BY
{ AssertLemma `set_lt_is_sp_of_leq` [] 
THEN Unfold `strict_part` (-1) 
THEN Trivial }

---

Latex:

---

Latex:
\mforall{}[p:PosetSig].  \mforall{}[a,b:|p|].    uiff(a  <p  b;(a  \mleq{}  b)  \mwedge{}  (\mneg{}(b  \mleq{}  a)))


By

---

Latex:
AssertLemma  `set\_lt\_is\_sp\_of\_leq`  [] 
THEN  Unfold  `strict\_part`  (-1) 
THEN  Trivial

---

Home Index