---

Step * of Lemma assert-lattice-ble

∀[l:LatticeStructure]. ∀[eq:EqDecider(Point(l))]. ∀[a,b:Point(l)].  uiff(↑lattice-ble(l;eq;a;b);a ≤ b)
BY
{ ((UnivCD THENA Auto) THEN RepUR ``lattice-ble lattice-le`` 0 THEN BoolCase ⌜eq a a ∧ b⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[l:LatticeStructure].  \mforall{}[eq:EqDecider(Point(l))].  \mforall{}[a,b:Point(l)].
    uiff(\muparrow{}lattice-ble(l;eq;a;b);a  \mleq{}  b)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepUR  ``lattice-ble  lattice-le``  0  THEN  BoolCase  \mkleeneopen{}eq  a  a  \mwedge{}  b\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index