---

Step * 1 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'
11. ∀c':Point. (c'=b=c ⇒ ac ≅ ac')
⊢ ∀c'@0:Point. (c'@0=b'=c' ⇒ a'c' ≅ a'c'@0)
BY
{ (RWO  "-4< -2< -3<" 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':Point.  (c'=b=c  {}\mRightarrow{}  ac  \00D0  ac')
\mvdash{}  \mforall{}c'@0:Point.  (c'@0=b'=c'  {}\mRightarrow{}  a'c'  \00D0  a'c'@0)


By

---

Latex:
(RWO    "-4<  -2<  -3<"  0  THEN  Auto)

---

Home Index