---

Step * of Lemma irrefl_trans_imp_sasym

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  (st_anti_sym(T;R)) supposing (trans(T;R) and irrefl(T;R))
BY
{ ((AGenRepD ["basic"] 
THENM D 0 ) THEN Auto) }

1
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. ∀[a:T]. (¬(R a a))
4. ∀a,b,c:T.  ((R a b) ⇒ (R b c) ⇒ (R a c))
5. x : T@i
6. y : T@i
7. R x y@i
8. R y x@i
⊢ False

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    (st\_anti\_sym(T;R))  supposing  (trans(T;R)  and  irrefl(T;R))


By

---

Latex:
((AGenRepD  ["basic"] 
THENM  D  0  )  THEN  Auto)

---

Home Index