---

Step * 2 of Lemma geo-out-interior-point-exists


1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. c' : Point
7. x : Point
8. a # bc
9. out(b aa')
10. out(b cc')
11. a-x-c
12. a leftof xb
⊢ ∃x':Point. (((a'-x'-c' ∧ out(b xx')) ∧ abx ≅a a'bx') ∧ cbx ≅a c'bx')
BY
{ ((InstLemma `left-between-implies-right2` [⌜g⌝;⌜x⌝;⌜b⌝;⌜a⌝;⌜c⌝]⋅ THENA EAuto 1)
   THEN (Assert c' leftof bx ∧ a' leftof xb BY
               ((InstLemma `geo-left-out-2` [⌜g⌝;⌜x⌝;⌜b⌝;⌜c⌝;⌜c'⌝]⋅ THENA Auto)
                THEN InstLemma `geo-left-out-3` [⌜g⌝;⌜b⌝;⌜x⌝;⌜a⌝;⌜a'⌝]⋅
                THEN Auto))
   ) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. c' : Point
7. x : Point
8. a # bc
9. out(b aa')
10. out(b cc')
11. a-x-c
12. a leftof xb
13. c leftof bx
14. c' leftof bx ∧ a' leftof xb
⊢ ∃x':Point. (((a'-x'-c' ∧ out(b xx')) ∧ abx ≅a a'bx') ∧ cbx ≅a c'bx')

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a'  :  Point
6.  c'  :  Point
7.  x  :  Point
8.  a  \#  bc
9.  out(b  aa')
10.  out(b  cc')
11.  a-x-c
12.  a  leftof  xb
\mvdash{}  \mexists{}x':Point.  (((a'-x'-c'  \mwedge{}  out(b  xx'))  \mwedge{}  abx  \mcong{}\msuba{}  a'bx')  \mwedge{}  cbx  \mcong{}\msuba{}  c'bx')


By

---

Latex:
((InstLemma  `left-between-implies-right2`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  EAuto  1)
  THEN  (Assert  c'  leftof  bx  \mwedge{}  a'  leftof  xb  BY
                          ((InstLemma  `geo-left-out-2`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  InstLemma  `geo-left-out-3`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{}]\mcdot{}
                            THEN  Auto))
  )

---

Home Index