---

Step * 2 1 3 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
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'
BY
{ (InstLemma `out-preserves-angle-cong_1` [⌜g⌝;⌜c⌝;⌜b⌝;⌜x⌝;⌜c⌝;⌜b⌝;⌜x⌝;⌜c⌝;⌜x⌝;⌜c'⌝;⌜x'⌝]⋅ THEN EAuto 1) }

---

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
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  \mcong{}\msuba{}  a'bx'
\mvdash{}  cbx  \mcong{}\msuba{}  c'bx'


By

---

Latex:
(InstLemma  `out-preserves-angle-cong\_1`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{}]\mcdot{}
  THEN  EAuto  1
  )

---

Home Index