---

Step * of Lemma geo-equilateral-exists

∀e:BasicGeometry-. ∀a,b,c:Point.  (a # bc ⇒ (∃x:Point. ((ax ≅ ac ∧ out(a bx)) ∧ a # xc)))
BY
{ ((Auto THEN (Assert a ≠ c ∧ b ≠ a BY (D -1 THEN FLemma `left-implies-sep` [-1] THEN EAuto 1)))
   THEN ((gProperProlong ⌜b⌝⌜a⌝`A'⌜O⌝⌜X⌝⋅ THENA Auto) THEN (gProperProlong ⌜A⌝⌜a⌝`a\''⌜a⌝⌜c⌝⋅ THENA EAuto 1))
   THEN ExRepD
   THEN D 0 With ⌜a'⌝ 
   THEN EAuto 1) }

1
1. e : BasicGeometry-
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. a ≠ c
7. b ≠ a
8. A : Point
9. b-a-A
10. aA ≅ OX
11. a' : Point
12. A-a-a'
13. aa' ≅ ac
14. aa' ≅ ac
⊢ out(a ba')

2
1. e : BasicGeometry-
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. a ≠ c
7. b ≠ a
8. A : Point
9. b-a-A
10. aA ≅ OX
11. a' : Point
12. A-a-a'
13. aa' ≅ ac
14. aa' ≅ ac
15. out(a ba')
⊢ a # a'c

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry-.  \mforall{}a,b,c:Point.    (a  \#  bc  {}\mRightarrow{}  (\mexists{}x:Point.  ((ax  \mcong{}  ac  \mwedge{}  out(a  bx))  \mwedge{}  a  \#  xc)))


By

---

Latex:
((Auto  THEN  (Assert  a  \mneq{}  c  \mwedge{}  b  \mneq{}  a  BY  (D  -1  THEN  FLemma  `left-implies-sep`  [-1]  THEN  EAuto  1)))
  THEN  ((gProperProlong  \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}`A'\mkleeneopen{}O\mkleeneclose{}\mkleeneopen{}X\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  (gProperProlong  \mkleeneopen{}A\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}`a\mbackslash{}''\mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}\mcdot{}  THENA  EAuto  1)
              )
  THEN  ExRepD
  THEN  D  0  With  \mkleeneopen{}a'\mkleeneclose{} 
  THEN  EAuto  1)

---

Home Index