---

Step * 2 1 1 of Lemma full-Pasch


1. e : EuclideanPlane
2. a : Point
3. x : Point
4. y : Point
5. d : Point
6. p : Point
7. d leftof ax
8. x-p-a
9. d # py
10. a leftof xy
11. y leftof ax
12. d leftof ap
13. d' : Point
14. d-p-d'
15. pd' ≅ dp
⊢ ∃p':Point. ((x-p'-y ∨ a-p'-y) ∧ Colinear(d;p;p'))
BY
{ ((Assert d' leftof pa BY
          (InstLemma `left-between-implies-right1` [⌜e⌝;⌜a⌝;⌜p⌝;⌜d⌝;⌜d'⌝]⋅ THEN Auto))
   THEN (Assert d' leftof xa BY
               (RepeatFor 2 ((FLemma `left-symmetry` [-1] THEN Auto))
                THEN (InstLemma `left-convex2` [⌜e⌝;⌜a⌝;⌜d'⌝;⌜p⌝;⌜x⌝]⋅ THEN Auto)
                THEN RepeatFor 2 ((FLemma `left-symmetry` [-1] THEN Auto))))
   ) }

1
1. e : EuclideanPlane
2. a : Point
3. x : Point
4. y : Point
5. d : Point
6. p : Point
7. d leftof ax
8. x-p-a
9. d # py
10. a leftof xy
11. y leftof ax
12. d leftof ap
13. d' : Point
14. d-p-d'
15. pd' ≅ dp
16. d' leftof pa
17. d' leftof xa
⊢ ∃p':Point. ((x-p'-y ∨ a-p'-y) ∧ Colinear(d;p;p'))

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  x  :  Point
4.  y  :  Point
5.  d  :  Point
6.  p  :  Point
7.  d  leftof  ax
8.  x-p-a
9.  d  \#  py
10.  a  leftof  xy
11.  y  leftof  ax
12.  d  leftof  ap
13.  d'  :  Point
14.  d-p-d'
15.  pd'  \00D0  dp
\mvdash{}  \mexists{}p':Point.  ((x-p'-y  \mvee{}  a-p'-y)  \mwedge{}  Colinear(d;p;p'))


By

---

Latex:
((Assert  d'  leftof  pa  BY
                (InstLemma  `left-between-implies-right1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}d'\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  (Assert  d'  leftof  xa  BY
                          (RepeatFor  2  ((FLemma  `left-symmetry`  [-1]  THEN  Auto))
                            THEN  (InstLemma  `left-convex2`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}d'\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)
                            THEN  RepeatFor  2  ((FLemma  `left-symmetry`  [-1]  THEN  Auto))))
  )

---

Home Index