---

Step * 2 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 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')
BY
{ ((InstLemma `use-plane-sep_strict` [⌜g⌝;⌜x⌝;⌜b⌝;⌜a'⌝;⌜c'⌝]⋅ THENA Auto)
   THEN (ExRepD THEN RenameVar `x\'' (-3))
   THEN D 0 With ⌜x'⌝ 
   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
15. a' leftof xb
16. x' : Point
17. Colinear(x;b;x')
18. a'-x'-c'
19. a'-x'-c'
⊢ out(b xx')

2
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
15. a' leftof xb
16. x' : Point
17. Colinear(x;b;x')
18. a'-x'-c'
19. a'-x'-c'
20. out(b xx')
⊢ abx ≅a a'bx'

3
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
15. a' leftof xb
16. x' : Point
17. Colinear(x;b;x')
18. a'-x'-c'
19. a'-x'-c'
20. out(b xx')
21. 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
13.  c  leftof  bx
14.  c'  leftof  bx  \mwedge{}  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  `use-plane-sep\_strict`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (ExRepD  THEN  RenameVar  `x\mbackslash{}''  (-3))
  THEN  D  0  With  \mkleeneopen{}x'\mkleeneclose{} 
  THEN  Auto)

---

Home Index