---

Step * of Lemma K_forces_connect_lemma

∀u,v,knd,K:Top.
  (K-forces(K;mFOconnect(knd;u;v)) ~ if knd =a "and" then λi,a. ((K-forces(K;u) i a) ∧ (K-forces(K;v) i a))
  if knd =a "or" then λi,a. ((K-forces(K;u) i a) ∨ (K-forces(K;v) i a))
  else λi,a. ∀j:{j:World| i ≤ j} . ((K-forces(K;u) j a) ⇒ (K-forces(K;v) j a))
  fi )
BY
{ ((Intros THEN Unfold `K-forces` 0 THEN Reduce 0) THEN EqCD) }

---

Latex:

---

Latex:
\mforall{}u,v,knd,K:Top.
    (K-forces(K;mFOconnect(knd;u;v))  \msim{}  if  knd  =a  "and"
                                                                              then  \mlambda{}i,a.  ((K-forces(K;u)  i  a)  \mwedge{}  (K-forces(K;v)  i  a))
    if  knd  =a  "or"  then  \mlambda{}i,a.  ((K-forces(K;u)  i  a)  \mvee{}  (K-forces(K;v)  i  a))
    else  \mlambda{}i,a.  \mforall{}j:\{j:World|  i  \mleq{}  j\}  .  ((K-forces(K;u)  j  a)  {}\mRightarrow{}  (K-forces(K;v)  j  a))
    fi  )


By

---

Latex:
((Intros  THEN  Unfold  `K-forces`  0  THEN  Reduce  0)  THEN  EqCD)

---

Home Index