---

Step * of Lemma dl-R_refl

∀K:dl_KS. ∀i:worlds(K).  iRi
BY
{ (Auto THEN GenConclTerm ⌜Rref(K;i)⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}K:dl\_KS.  \mforall{}i:worlds(K).    iRi


By

---

Latex:
(Auto  THEN  GenConclTerm  \mkleeneopen{}Rref(K;i)\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index