---

Step * 1 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'
⊢ {Rabc ⇐⇒ Ra'b'c'}
BY
{ ((RepeatFor 2 (D 0) THENA Auto) THEN ParallelLast) }

1
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':Point. (c'=b=c ⇒ ac ≅ ac')
⊢ ∀c'@0:Point. (c'@0=b'=c' ⇒ a'c' ≅ a'c'@0)

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)
⊢ ∀c':Point. (c'=b=c ⇒ ac ≅ ac')

---

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'
\mvdash{}  \{Rabc  \mLeftarrow{}{}\mRightarrow{}  Ra'b'c'\}


By

---

Latex:
((RepeatFor  2  (D  0)  THENA  Auto)  THEN  ParallelLast)

---

Home Index