---

Step * of Lemma Euclid-Prop16-construction-lemma

∀g:EuclideanPlane. ∀a,b,c:Point.
  (a # bc ⇒ (∃x:{x:Point| b=x=c} . ∃y:{y:Point| a=x=y} . (abc ≅a ycb ∧ (b ≠ x ∧ x ≠ c) ∧ a ≠ x ∧ x ≠ y)))
BY
{ ((Auto THEN ((InstLemma `Euclid-midpoint` [⌜g⌝;⌜b⌝;⌜c⌝]⋅ THEN Auto) THEN ExRepD) THEN D 0 With ⌜d⌝  THEN Auto)
   THEN (InstLemma `colinear-lsep` [⌜g⌝;⌜b⌝;⌜c⌝;⌜a⌝;⌜d⌝]⋅ THENA EAuto 1)
   THEN ((((gProperProlong ⌜a⌝⌜d⌝`y'⌜a⌝⌜d⌝⋅ THEN Auto) THEN ExRepD) THEN D 0 With ⌜y⌝  THEN Auto)
         THENW (MemTypeCD THEN EAuto 1)
         )) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. d : Point
7. b=d=c
8. d # ca
9. y : Point
10. a-d-y
11. dy ≅ ad
⊢ abc ≅a ycb

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c:Point.
    (a  \#  bc
    {}\mRightarrow{}  (\mexists{}x:\{x:Point|  b=x=c\}  .  \mexists{}y:\{y:Point|  a=x=y\}  .  (abc  \mcong{}\msuba{}  ycb  \mwedge{}  (b  \mneq{}  x  \mwedge{}  x  \mneq{}  c)  \mwedge{}  a  \mneq{}  x  \mwedge{}  x  \mneq{}  y)))


By

---

Latex:
((Auto
    THEN  ((InstLemma  `Euclid-midpoint`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  ExRepD)
    THEN  D  0  With  \mkleeneopen{}d\mkleeneclose{} 
    THEN  Auto)
  THEN  (InstLemma  `colinear-lsep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THENA  EAuto  1)
  THEN  ((((gProperProlong  \mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}d\mkleeneclose{}`y'\mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}d\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  ExRepD)  THEN  D  0  With  \mkleeneopen{}y\mkleeneclose{}    THEN  Auto)
              THENW  (MemTypeCD  THEN  EAuto  1)
              ))

---

Home Index