---

Step * of Lemma K_uforces_connect_lemma

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

---

Latex:

---

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


By

---

Latex:
(Intros  THEN  Unfold  `K-uforces`  0  THEN  Reduce  0  THEN  Auto)

---

Home Index