---

Step * of Lemma right-angles-not-complementary

∀e:BasicGeometry. ∀a,b,c:Point.  (Rabc ⇒ Racb ⇒ b ≡ c)
BY
{ (Auto
   THEN gSeparatedCases ⌜b⌝ ⌜c⌝⋅
   THEN Auto
   THEN gSymmetricPoint ⌜b⌝ ⌜c⌝ `c\''⋅
   THEN (FLemma `geo-midpoint-symmetry` [-1] THENA Auto)
   THEN (gSeparatedCases' ⌜a⌝ ⌜c⌝⋅ THENA Auto)
   THEN gSymmetricPoint ⌜c⌝ ⌜a⌝ `a\''⋅
   THEN (FLemma `geo-midpoint-symmetry` [-1] THENA Auto)) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. Rabc
6. Racb
7. b ≠ c
8. c' : Point
9. c=b=c'
10. c'=b=c
11. a ≠ c
12. a' : Point
13. a=c=a'
14. a'=c=a
⊢ b ≡ c

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c:Point.    (Rabc  {}\mRightarrow{}  Racb  {}\mRightarrow{}  b  \mequiv{}  c)


By

---

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

---

Home Index