---

Step * of Lemma refl_cl_is_order

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  trans(T;R) ⇒ order(T;Ro) supposing irrefl(T;R)
BY
{ ((Unfold `xxorder` 0 THEN AGenRepD ["basic";"compound"] 
THENM OnAll (Eval ``refl_cl``)) THENA 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))@i
5. a : T@i
⊢ (a = a ∈ T) ∨ (R a a)

2
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))@i
5. a : T@i
6. b : T@i
7. c : T@i
8. (a = b ∈ T) ∨ (R a b)@i
9. (b = c ∈ T) ∨ (R b c)@i
⊢ (a = c ∈ T) ∨ (R a c)

3
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))@i
5. x : T@i
6. y : T@i
7. (x = y ∈ T) ∨ (R x y)@i
8. (y = x ∈ T) ∨ (R y x)@i
⊢ x = y ∈ T

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    trans(T;R)  {}\mRightarrow{}  order(T;R\msupzero{})  supposing  irrefl(T;R)


By

---

Latex:
((Unfold  `xxorder`  0  THEN  AGenRepD  ["basic";"compound"] 
THENM  OnAll  (Eval  ``refl\_cl``))  THENA  Auto)

---

Home Index