---

Step * 1 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. c : Point
24. d : Point
25. fc ≅ fX ∧ fd ≅ fX ∧ gc ≅ gh ∧ gd ≅ gh ∧ c leftof fg ∧ d leftof gf
⊢ ∃a,b,c:Point. (((a # bc ∧ ab ≅ a1a2) ∧ bc ≅ b1b2) ∧ ca ≅ c1c2)
BY
{ (InstConcl [⌜c⌝;⌜f⌝;⌜g⌝]⋅ THEN Auto) }

---

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.  c  :  Point
24.  d  :  Point
25.  fc  \mcong{}  fX  \mwedge{}  fd  \mcong{}  fX  \mwedge{}  gc  \mcong{}  gh  \mwedge{}  gd  \mcong{}  gh  \mwedge{}  c  leftof  fg  \mwedge{}  d  leftof  gf
\mvdash{}  \mexists{}a,b,c:Point.  (((a  \#  bc  \mwedge{}  ab  \mcong{}  a1a2)  \mwedge{}  bc  \mcong{}  b1b2)  \mwedge{}  ca  \mcong{}  c1c2)


By

---

Latex:
(InstConcl  [\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}g\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index