---

Step * 1 of Lemma refl_cl_sp_le_rel


1. [T] : Type
2. [r] : T ⟶ T ⟶ ℙ
3. ∀a:T. (r a a)
4. x : T
5. y : T
6. (x = y ∈ T) ∨ ((r x y) ∧ (¬(r y x)))
⊢ r x y
BY
{ ((D 6) THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [r]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}a:T.  (r  a  a)
4.  x  :  T
5.  y  :  T
6.  (x  =  y)  \mvee{}  ((r  x  y)  \mwedge{}  (\mneg{}(r  y  x)))
\mvdash{}  r  x  y


By

---

Latex:
((D  6)  THEN  Auto)

---

Home Index