---

Step * 1 1 of Lemma set_lt_is_sp_of_leq


1. p : PosetSig
2. a : |p|
3. b : |p|
⊢ uiff(↑((a (≤b) b) ∧b (¬b(b (≤b) a)));(a ≤ b) ∧ (¬(b ≤ a)))
BY
{ (RW bool_to_propC 0 THEN Auto) }

---

Latex:

---

Latex:

1.  p  :  PosetSig
2.  a  :  |p|
3.  b  :  |p|
\mvdash{}  uiff(\muparrow{}((a  (\mleq{}\msubb{})  b)  \mwedge{}\msubb{}  (\mneg{}\msubb{}(b  (\mleq{}\msubb{})  a)));(a  \mleq{}  b)  \mwedge{}  (\mneg{}(b  \mleq{}  a)))


By

---

Latex:
(RW  bool\_to\_propC  0  THEN  Auto)

---

Home Index