---

Step * 1 of Lemma Prop23-construction-lemma


1. e : EuclideanPlane
2. p : Point
3. q : Point
4. r : Point
5. a : Point
6. a' : Point
7. p # qr
8. a ≠ a'
9. |qr| < |qp| + |pr|
10. |pr| < |qp| + |qr|
11. |qp| < |pr| + |qr|
12. P : Point
13. a'-a-P
14. aP ≅ OX
15. b : Point
16. P-a-b
17. ab ≅ pq
18. out(a a'b)
⊢ ∃c1,c2:Point. (((pq ≅ ab ∧ out(a a'b)) ∧ pr ≅ ac1 ∧ bc2 > bc1) ∧ qr ≅ bc2 ∧ ac1 > ac2)
BY
{ ((InstLemma `Prop22-symmetric-point-construction-lemma` [⌜e⌝;⌜p⌝;⌜q⌝;⌜r⌝]⋅ THENA Auto) THEN ExRepD) }

1
1. e : EuclideanPlane
2. p : Point
3. q : Point
4. r : Point
5. a : Point
6. a' : Point
7. p # qr
8. a ≠ a'
9. |qr| < |qp| + |pr|
10. |pr| < |qp| + |qr|
11. |qp| < |pr| + |qr|
12. P : Point
13. a'-a-P
14. aP ≅ OX
15. b : Point
16. P-a-b
17. ab ≅ pq
18. out(a a'b)
19. c1 : Point
20. c1' : Point
21. c1'' : Point
22. c2 : Point
23. c2' : Point
24. c2'' : Point
25. pc1 ≅ pr
26. out(p qc1)
27. qc2 ≅ qr
28. out(q pc2)
29. q-p-c1'
30. pc1' ≅ pc1
31. p-q-c2'
32. qc2' ≅ qc2
33. p_q_c1''
34. qc1'' ≅ qc1
35. q_p_c2''
36. pc2'' ≅ pc2
37. p-c1-c2'
38. q-c2-c1'
39. c1'-p-c1
40. c2'-q-c2
41. c1'-c2-c2'
42. c2'-c1-c1'
43. c1'-c2-c1
44. c2'-c1-c2
⊢ ∃c1,c2:Point. (((pq ≅ ab ∧ out(a a'b)) ∧ pr ≅ ac1 ∧ bc2 > bc1) ∧ qr ≅ bc2 ∧ ac1 > ac2)

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  p  :  Point
3.  q  :  Point
4.  r  :  Point
5.  a  :  Point
6.  a'  :  Point
7.  p  \#  qr
8.  a  \mneq{}  a'
9.  |qr|  <  |qp|  +  |pr|
10.  |pr|  <  |qp|  +  |qr|
11.  |qp|  <  |pr|  +  |qr|
12.  P  :  Point
13.  a'-a-P
14.  aP  \mcong{}  OX
15.  b  :  Point
16.  P-a-b
17.  ab  \mcong{}  pq
18.  out(a  a'b)
\mvdash{}  \mexists{}c1,c2:Point.  (((pq  \mcong{}  ab  \mwedge{}  out(a  a'b))  \mwedge{}  pr  \mcong{}  ac1  \mwedge{}  bc2  >  bc1)  \mwedge{}  qr  \mcong{}  bc2  \mwedge{}  ac1  >  ac2)


By

---

Latex:
((InstLemma  `Prop22-symmetric-point-construction-lemma`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  ExRepD)

---

Home Index