---

Step * 1 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 bx
⊢ ∃x':Point. (((a'-x'-c' ∧ out(b xx')) ∧ abx ≅a a'bx') ∧ cbx ≅a c'bx')
BY
{ ((InstLemma `left-between-implies-right1` [⌜g⌝;⌜b⌝;⌜x⌝;⌜a⌝;⌜c⌝]⋅ THENA EAuto 1)
   THEN (Assert c' leftof xb ∧ a' leftof bx BY
               ((InstLemma `geo-left-out-2` [⌜g⌝;⌜x⌝;⌜b⌝;⌜a⌝;⌜a'⌝]⋅ THENA Auto)
                THEN InstLemma `geo-left-out-3` [⌜g⌝;⌜b⌝;⌜x⌝;⌜c⌝;⌜c'⌝]⋅
                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 bx
13. c leftof xb
14. c' leftof xb ∧ a' leftof bx
⊢ ∃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  bx
\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-right1`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  EAuto  1)
  THEN  (Assert  c'  leftof  xb  \mwedge{}  a'  leftof  bx  BY
                          ((InstLemma  `geo-left-out-2`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  InstLemma  `geo-left-out-3`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{}]\mcdot{}
                            THEN  Auto))
  )

---

Home Index