---

Step * 1 1 2 1 2 2 of Lemma Euclid-Prop22


1. e : EuclideanPlane
2. a1 : Point
3. a2 : Point
4. b1 : Point
5. b2 : Point
6. c1 : Point
7. c2 : Point
8. |a1a2| < |b1b2| + |c1c2|
9. |b1b2| < |a1a2| + |c1c2|
10. |c1c2| < |a1a2| + |b1b2|
11. a1 # a2
12. b1 # b2
13. c1 # c2
14. f : Point
15. O-X-f
16. Xf ≅ a1a2
17. g : Point
18. X-f-g
19. fg ≅ b1b2
20. h : Point
21. f-g-h
22. gh ≅ c1c2
23. x' : Point
24. X-f-x'
25. Xf ≅ fx'
26. f-x'-h
27. h' : Point
28. h-g-h'
29. gh ≅ gh'
30. X-h'-h
⊢ ∃p,q:Point. ((fX ≅ fp ∧ gh>gp) ∧ gh ≅ gq ∧ fX>fq)
BY
{ (Assert X-h'-x' BY
         ((Assert out(X h'x') BY
                 ((Assert out(X h'h) BY
                         (InstLemma `geo-between-out` [⌜e⌝;⌜X⌝;⌜h'⌝;⌜h⌝]⋅ THEN Auto))
                  THEN (Assert out(X hx') BY
                              (InstLemma `geo-between-out` [⌜e⌝;⌜X⌝;⌜x'⌝;⌜h⌝]⋅ THEN EAuto 1))
                  THEN InstLemma `geo-out_transitivity` [⌜e⌝;⌜X⌝;⌜h'⌝;⌜h⌝;⌜x'⌝]⋅
                  THEN Auto))
          THEN InstLemma `geo-lt-out-to-between` [⌜e⌝;⌜X⌝;⌜h'⌝;⌜x'⌝]⋅
          THEN Auto)) }

1
.....aux..... 
1. e : EuclideanPlane
2. a1 : Point
3. a2 : Point
4. b1 : Point
5. b2 : Point
6. c1 : Point
7. c2 : Point
8. |a1a2| < |b1b2| + |c1c2|
9. |b1b2| < |a1a2| + |c1c2|
10. |c1c2| < |a1a2| + |b1b2|
11. a1 # a2
12. b1 # b2
13. c1 # c2
14. f : Point
15. O-X-f
16. Xf ≅ a1a2
17. g : Point
18. X-f-g
19. fg ≅ b1b2
20. h : Point
21. f-g-h
22. gh ≅ c1c2
23. x' : Point
24. X-f-x'
25. Xf ≅ fx'
26. f-x'-h
27. h' : Point
28. h-g-h'
29. gh ≅ gh'
30. X-h'-h
31. out(X h'x')
⊢ |Xh'| < |Xx'|

2
1. e : EuclideanPlane
2. a1 : Point
3. a2 : Point
4. b1 : Point
5. b2 : Point
6. c1 : Point
7. c2 : Point
8. |a1a2| < |b1b2| + |c1c2|
9. |b1b2| < |a1a2| + |c1c2|
10. |c1c2| < |a1a2| + |b1b2|
11. a1 # a2
12. b1 # b2
13. c1 # c2
14. f : Point
15. O-X-f
16. Xf ≅ a1a2
17. g : Point
18. X-f-g
19. fg ≅ b1b2
20. h : Point
21. f-g-h
22. gh ≅ c1c2
23. x' : Point
24. X-f-x'
25. Xf ≅ fx'
26. f-x'-h
27. h' : Point
28. h-g-h'
29. gh ≅ gh'
30. X-h'-h
31. X-h'-x'
⊢ ∃p,q:Point. ((fX ≅ fp ∧ gh>gp) ∧ gh ≅ gq ∧ fX>fq)

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a1  :  Point
3.  a2  :  Point
4.  b1  :  Point
5.  b2  :  Point
6.  c1  :  Point
7.  c2  :  Point
8.  |a1a2|  <  |b1b2|  +  |c1c2|
9.  |b1b2|  <  |a1a2|  +  |c1c2|
10.  |c1c2|  <  |a1a2|  +  |b1b2|
11.  a1  \#  a2
12.  b1  \#  b2
13.  c1  \#  c2
14.  f  :  Point
15.  O-X-f
16.  Xf  \mcong{}  a1a2
17.  g  :  Point
18.  X-f-g
19.  fg  \mcong{}  b1b2
20.  h  :  Point
21.  f-g-h
22.  gh  \mcong{}  c1c2
23.  x'  :  Point
24.  X-f-x'
25.  Xf  \mcong{}  fx'
26.  f-x'-h
27.  h'  :  Point
28.  h-g-h'
29.  gh  \mcong{}  gh'
30.  X-h'-h
\mvdash{}  \mexists{}p,q:Point.  ((fX  \mcong{}  fp  \mwedge{}  gh>gp)  \mwedge{}  gh  \mcong{}  gq  \mwedge{}  fX>fq)


By

---

Latex:
(Assert  X-h'-x'  BY
              ((Assert  out(X  h'x')  BY
                              ((Assert  out(X  h'h)  BY
                                              (InstLemma  `geo-between-out`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}h'\mkleeneclose{};\mkleeneopen{}h\mkleeneclose{}]\mcdot{}  THEN  Auto))
                                THEN  (Assert  out(X  hx')  BY
                                                        (InstLemma  `geo-between-out`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}h\mkleeneclose{}]\mcdot{}  THEN  EAuto  1))
                                THEN  InstLemma  `geo-out\_transitivity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}h'\mkleeneclose{};\mkleeneopen{}h\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{}]\mcdot{}
                                THEN  Auto))
                THEN  InstLemma  `geo-lt-out-to-between`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}h'\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{}]\mcdot{}
                THEN  Auto))

---

Home Index