Step
*
2
of Lemma
geo-triangle_functionality
1. e : HeytingGeometry
2. ∀a1,a2,b1,b2,c1,c2:Point. (a1 ≡ a2
⇒ b1 ≡ b2
⇒ c1 ≡ c2
⇒ a1 # b1c1
⇒ a2 # b2c2)
⊢ ∀a1,a2,b1,b2,c1,c2:Point. (a1 ≡ a2
⇒ b1 ≡ b2
⇒ c1 ≡ c2
⇒ (a1 # b1c1
⇐⇒ a2 # b2c2))
BY
{ Auto }
1
1. e : HeytingGeometry
2. ∀a1,a2,b1,b2,c1,c2:Point. (a1 ≡ a2
⇒ b1 ≡ b2
⇒ c1 ≡ c2
⇒ a1 # b1c1
⇒ a2 # b2c2)
3. a1 : Point
4. a2 : Point
5. b1 : Point
6. b2 : Point
7. c1 : Point
8. c2 : Point
9. a1 ≡ a2
10. b1 ≡ b2
11. c1 ≡ c2
12. a2 # b2c2
⊢ a1 # b1c1
Latex:
Latex:
1. e : HeytingGeometry
2. \mforall{}a1,a2,b1,b2,c1,c2:Point. (a1 \mequiv{} a2 {}\mRightarrow{} b1 \mequiv{} b2 {}\mRightarrow{} c1 \mequiv{} c2 {}\mRightarrow{} a1 \# b1c1 {}\mRightarrow{} a2 \# b2c2)
\mvdash{} \mforall{}a1,a2,b1,b2,c1,c2:Point. (a1 \mequiv{} a2 {}\mRightarrow{} b1 \mequiv{} b2 {}\mRightarrow{} c1 \mequiv{} c2 {}\mRightarrow{} (a1 \# b1c1 \mLeftarrow{}{}\mRightarrow{} a2 \# b2c2))
By
Latex:
Auto
Home
Index