---

Step * 2 of Lemma rel_exp_one


1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. x : T
4. y : T
5. x R y
⊢ (∃z:T. (0 < 1 c∧ ((x R^0 z) ∧ (z R y)))) ∨ ((1 = 0 ∈ ℤ) ∧ (x = y ∈ T))
BY
{ RW (SweepDnC RelExp0C) 0 }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. x : T
4. y : T
5. x R y
⊢ (∃z:T. (0 < 1 c∧ ((x = z ∈ T) ∧ (z R y)))) ∨ ((1 = 0 ∈ ℤ) ∧ (x = y ∈ T))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [R]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  x  :  T
4.  y  :  T
5.  x  R  y
\mvdash{}  (\mexists{}z:T.  (0  <  1  c\mwedge{}  ((x  rel\_exp(T;  R;  0)  z)  \mwedge{}  (z  R  y))))  \mvee{}  ((1  =  0)  \mwedge{}  (x  =  y))


By

---

Latex:
RW  (SweepDnC  RelExp0C)  0

---

Home Index