---

Step * 1 of Lemma rel_le_sp_refl_cl


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

1
1. [T] : Type
2. [r] : T ⟶ T ⟶ ℙ
3. ∀[a:T]. (¬(r a a))
4. ∀x,y:T.  (¬((r x y) ∧ (r y x)))
5. x : T@i
6. y : T@i
7. r x y@i
⊢ (x = y ∈ T) ∨ (r x y)

2
1. [T] : Type
2. [r] : T ⟶ T ⟶ ℙ
3. ∀[a:T]. (¬(r a a))
4. ∀x,y:T.  (¬((r x y) ∧ (r y x)))
5. x : T@i
6. y : T@i
7. r x y@i
⊢ ¬((y = x ∈ T) ∨ (r y x))

---

Latex:

---

Latex:

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


By

---

Latex:
((D  0)  THENA  Auto)

---

Home Index