---

Step * 1 1 of Lemma ancestral-logic-lemma1

.....assertion..... 
⊢ ∀x,y:Dom.  ((R x y) ⇒ ((R x y) ∨ (∃z:Dom. ((R x z) ∧ TC(λa,b.R a b)(z,y)))))
BY
{ (RepeatFor 2 (FOAllIntro) THEN FOImpliesIntro THEN FOOrIntroLeft) }

1
9. x : Dom@i
10. y : Dom@i
11. R x y@i
⊢ R x y

---

Latex:


.....assertion..... 
\mvdash{}  \mforall{}x,y:Dom.    ((R  x  y)  {}\mRightarrow{}  ((R  x  y)  \mvee{}  (\mexists{}z:Dom.  ((R  x  z)  \mwedge{}  TC(\mlambda{}a,b.R  a  b)(z,y)))))


By

(RepeatFor  2  (FOAllIntro)  THEN  FOImpliesIntro  THEN  FOOrIntroLeft)

---

Home Index