---

Step * 1 2 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
8. y = x ∈ T@i
⊢ False
BY
{ ((RWW "8" 7 THENM Negate 7 
THENM BHyp 3) THEN Auto) }

---

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
8.  y  =  x@i
\mvdash{}  False


By

---

Latex:
((RWW  "8"  7  THENM  Negate  7 
THENM  BHyp  3)  THEN  Auto)

---

Home Index