---

Step * of Lemma rel-is-immediate

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  (∀x,y:T.  (R x y ⇐⇒ R+! x y)) supposing 
     ((∀a,b,c:T.  (((R a b) ∧ (R a c)) ⇒ (b = c ∈ T))) and 
     (∀x,y:T.  ((R+ x y) ⇒ (¬(R+ y x)))))
BY
{ Auto }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. ∀x,y:T.  ((R+ x y) ⇒ (¬(R+ y x)))
4. ∀a,b,c:T.  (((R a b) ∧ (R a c)) ⇒ (b = c ∈ T))
5. x : T
6. y : T
7. R x y
⊢ R+! x y

2
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. ∀x,y:T.  ((R+ x y) ⇒ (¬(R+ y x)))
4. ∀a,b,c:T.  (((R a b) ∧ (R a c)) ⇒ (b = c ∈ T))
5. x : T
6. y : T
7. R+! x y
⊢ R x y

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (\mforall{}x,y:T.    (R  x  y  \mLeftarrow{}{}\mRightarrow{}  R\msupplus{}!  x  y))  supposing 
          ((\mforall{}a,b,c:T.    (((R  a  b)  \mwedge{}  (R  a  c))  {}\mRightarrow{}  (b  =  c)))  and 
          (\mforall{}x,y:T.    ((R\msupplus{}  x  y)  {}\mRightarrow{}  (\mneg{}(R\msupplus{}  y  x)))))


By

---

Latex:
Auto

---

Home Index