---

Step * of Lemma Euclid-Prop23_half-plane2

No Annotations
∀e:EuclideanPlane. ∀a,b,x,y,z:Point.  (z # xy ⇒ a # b ⇒ (∃x',b':Point. (out(a bb') ∧ x' leftof b'a ∧ x'ab' ≅a zxy)))
BY
{ (Auto
   THEN (InstLemma `Euclid-Prop20_cycle` [⌜e⌝;⌜x⌝;⌜y⌝;⌜z⌝]⋅ THENA Auto)
   THEN ((InstLemma `Prop23-construction-lemma` [⌜e⌝;⌜x⌝;⌜y⌝;⌜z⌝;⌜a⌝;⌜b⌝]⋅ THENA Auto) THEN ExRepD)
   THEN RenameVar `b1' (12)
   THEN GenConclTerm ⌜geo-CCR(e;a;c1;b1;c2)⌝⋅
   THEN Auto) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. x : Point
5. y : Point
6. z : Point
7. z # xy
8. a # b
9. |yz| < |yx| + |xz|
10. |xz| < |yx| + |yz|
11. |yx| < |xz| + |yz|
12. b1 : Point
13. c1 : Point
14. c2 : Point
15. xy ≅ ab1
16. out(a bb1)
17. xz ≅ ac1
18. b1c2 > b1c1
19. yz ≅ b1c2
20. ac1 > ac2
⊢ ∃p,q:Point. ((ac1 ≅ ap ∧ b1c2>b1p) ∧ b1c2 ≅ b1q ∧ ac1>aq)

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. x : Point
5. y : Point
6. z : Point
7. z # xy
8. a # b
9. |yz| < |yx| + |xz|
10. |xz| < |yx| + |yz|
11. |yx| < |xz| + |yz|
12. b1 : Point
13. c1 : Point
14. c2 : Point
15. xy ≅ ab1
16. out(a bb1)
17. xz ≅ ac1
18. b1c2 > b1c1
19. yz ≅ b1c2
20. ac1 > ac2
21. v : {v:Point| ac1 ≅ av ∧ b1c2 ≅ b1v ∧ v leftof b1a} 
22. geo-CCR(e;a;c1;b1;c2) = v ∈ {v:Point| ac1 ≅ av ∧ b1c2 ≅ b1v ∧ v leftof b1a} 
⊢ ∃x',b':Point. (out(a bb') ∧ x' leftof b'a ∧ x'ab' ≅a zxy)

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,b,x,y,z:Point.
    (z  \#  xy  {}\mRightarrow{}  a  \#  b  {}\mRightarrow{}  (\mexists{}x',b':Point.  (out(a  bb')  \mwedge{}  x'  leftof  b'a  \mwedge{}  x'ab'  \mcong{}\msuba{}  zxy)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `Euclid-Prop20\_cycle`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ((InstLemma  `Prop23-construction-lemma`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  ExRepD)
  THEN  RenameVar  `b1'  (12)
  THEN  GenConclTerm  \mkleeneopen{}geo-CCR(e;a;c1;b1;c2)\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index