---

Step * 1 2 of Lemma right-angle_functionality


1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. b' : Point
7. c' : Point
8. a ≡ a'
9. b ≡ b'
10. c ≡ c'
11. ∀c'@0:Point. (c'@0=b'=c' ⇒ a'c' ≅ a'c'@0)
⊢ ∀c':Point. (c'=b=c ⇒ ac ≅ ac')
BY
{ RepeatFor 2 (ParallelLast) }

1
.....antecedent..... 
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. b' : Point
7. c' : Point
8. a ≡ a'
9. b ≡ b'
10. c ≡ c'
11. ∀c'@0:Point. (c'@0=b'=c' ⇒ a'c' ≅ a'c'@0)
12. c1 : Point
13. c1=b=c
⊢ c1=b'=c'

2
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. b' : Point
7. c' : Point
8. a ≡ a'
9. b ≡ b'
10. c ≡ c'
11. ∀c'@0:Point. (c'@0=b'=c' ⇒ a'c' ≅ a'c'@0)
12. c1 : Point
13. c1=b=c
14. a'c' ≅ a'c1
⊢ ac ≅ ac1

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a'  :  Point
6.  b'  :  Point
7.  c'  :  Point
8.  a  \mequiv{}  a'
9.  b  \mequiv{}  b'
10.  c  \mequiv{}  c'
11.  \mforall{}c'@0:Point.  (c'@0=b'=c'  {}\mRightarrow{}  a'c'  \00D0  a'c'@0)
\mvdash{}  \mforall{}c':Point.  (c'=b=c  {}\mRightarrow{}  ac  \00D0  ac')


By

---

Latex:
RepeatFor  2  (ParallelLast)

---

Home Index