---

Step * of Lemma K-le_transitivity

∀K:mKripkeStruct. ∀i,j,k:World.  (i ≤ j ⇒ j ≤ k ⇒ i ≤ k)
BY
{ ((Unfold `K-le` 0 THEN Unfold `K-world` 0) THEN (D 0 THENA Auto) THEN DKripke 1 THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}K:mKripkeStruct.  \mforall{}i,j,k:World.    (i  \mleq{}  j  {}\mRightarrow{}  j  \mleq{}  k  {}\mRightarrow{}  i  \mleq{}  k)


By

---

Latex:
((Unfold  `K-le`  0  THEN  Unfold  `K-world`  0)
  THEN  (D  0  THENA  Auto)
  THEN  DKripke  1
  THEN  Reduce  0
  THEN  Auto)

---

Home Index