---

Step * of Lemma adjacent-right-angles

∀e:BasicGeometry. ∀a,b,c,a':Point.  (b ≠ c ⇒ Rabc ⇒ Ra'bc ⇒ Colinear(a;b;a'))
BY
{ (Auto
   THEN gSymmetricPoint ⌜b⌝⌜c⌝`c\''⋅
   THEN (FLemma `geo-midpoint-symmetry` [-1] THENA Auto)
   THEN (Assert ac ≅ ac' BY
               Auto)
   THEN (Assert a'c ≅ a'c' BY
               Auto)) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. b ≠ c
7. Rabc
8. Ra'bc
9. c' : Point
10. c=b=c'
11. c'=b=c
12. ac ≅ ac'
13. a'c ≅ a'c'
⊢ Colinear(a;b;a')

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,a':Point.    (b  \mneq{}  c  {}\mRightarrow{}  Rabc  {}\mRightarrow{}  Ra'bc  {}\mRightarrow{}  Colinear(a;b;a'))


By

---

Latex:
(Auto
  THEN  gSymmetricPoint  \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}`c\mbackslash{}''\mcdot{}
  THEN  (FLemma  `geo-midpoint-symmetry`  [-1]  THENA  Auto)
  THEN  (Assert  ac  \mcong{}  ac'  BY
                          Auto)
  THEN  (Assert  a'c  \mcong{}  a'c'  BY
                          Auto))

---

Home Index