---

Step * 1 2 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)
12. c1 : Point
13. c1=b=c
14. a'c' ≅ a'c1
⊢ ac ≅ ac1
BY
{ (RWO  "8 9 10" 0 THEN Auto) }

---

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)
12.  c1  :  Point
13.  c1=b=c
14.  a'c'  \00D0  a'c1
\mvdash{}  ac  \00D0  ac1


By

---

Latex:
(RWO    "8  9  10"  0  THEN  Auto)

---

Home Index