---

Step * 1 1 2 1 of Lemma cond_rel_equivalent

.....assertion..... 
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. [Q] : T ⟶ T ⟶ ℙ
4. [P] : T ⟶ ℙ
5. Trans(T;x,y.Q x y)@i
6. ∀x,y:T.  ((Q x y) ⇒ (¬(Q y x)))
7. R => Q@i
8. ∀x,y:T.  (((P x) ∧ (P y)) ⇒ (((R x y) ∨ (x = y ∈ T)) ∨ (R y x)))@i
9. x : T@i
10. y : T@i
11. P x@i
12. P y@i
13. Q x y@i
14. R y x
⊢ Q y x
BY
{ FinishThruSomeHyp Auto }

---

Latex:

---

Latex:
.....assertion..... 
1.  [T]  :  Type
2.  [R]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  [Q]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
4.  [P]  :  T  {}\mrightarrow{}  \mBbbP{}
5.  Trans(T;x,y.Q  x  y)@i
6.  \mforall{}x,y:T.    ((Q  x  y)  {}\mRightarrow{}  (\mneg{}(Q  y  x)))
7.  R  =>  Q@i
8.  \mforall{}x,y:T.    (((P  x)  \mwedge{}  (P  y))  {}\mRightarrow{}  (((R  x  y)  \mvee{}  (x  =  y))  \mvee{}  (R  y  x)))@i
9.  x  :  T@i
10.  y  :  T@i
11.  P  x@i
12.  P  y@i
13.  Q  x  y@i
14.  R  y  x
\mvdash{}  Q  y  x


By

---

Latex:
FinishThruSomeHyp  Auto

---

Home Index