Step
*
1
1
of Lemma
connex_functionality_wrt_implies
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. [R'] : T ⟶ T ⟶ ℙ
4. ∀x,y:T. {R[x;y]
⇒ R'[x;y]}
5. ∀x,y:T. (R[x;y] ∨ R[y;x])
6. x : T
7. y : T
⊢ R'[x;y] ∨ R'[y;x]
BY
{ (RWH (HypC 4) 5 THENA Auto) }
1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. [R'] : T ⟶ T ⟶ ℙ
4. ∀x,y:T. {R[x;y]
⇒ R'[x;y]}
5. ∀x,y:T. (R'[x;y] ∨ R'[y;x])
6. x : T
7. y : T
⊢ R'[x;y] ∨ R'[y;x]
Latex:
Latex:
1. [T] : Type
2. [R] : T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}
3. [R'] : T {}\mrightarrow{} T {}\mrightarrow{} \mBbbP{}
4. \mforall{}x,y:T. \{R[x;y] {}\mRightarrow{} R'[x;y]\}
5. \mforall{}x,y:T. (R[x;y] \mvee{} R[y;x])
6. x : T
7. y : T
\mvdash{} R'[x;y] \mvee{} R'[y;x]
By
Latex:
(RWH (HypC 4) 5 THENA Auto)
Home
Index