---

Step * 1 3 of Lemma out-preserves-angle-cong_1


1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. b' : Point
7. c' : Point
8. p : Point
9. q : Point
10. p' : Point
11. q' : Point
12. abc ≅a a'b'c'
13. out(b cq)
14. out(b ap)
15. out(b' c'q')
16. out(b' a'p')
17. a1 : Point
18. c1 : Point
19. x' : Point
20. z' : Point
21. out(b a1a)
22. out(b c1c)
23. out(b' x'a')
24. out(b' z'c')
25. a1bc1 ≅a x'b'z'
26. a1b ≅ x'b'
27. bc1 ≅ b'z'
28. c1a1 ≅ z'x'
⊢ out(b' x'p')
BY
{ (InstLemma `geo-out_transitivity` [⌜e⌝;⌜b'⌝;⌜x'⌝;⌜a'⌝;⌜p'⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a'  :  Point
6.  b'  :  Point
7.  c'  :  Point
8.  p  :  Point
9.  q  :  Point
10.  p'  :  Point
11.  q'  :  Point
12.  abc  \mcong{}\msuba{}  a'b'c'
13.  out(b  cq)
14.  out(b  ap)
15.  out(b'  c'q')
16.  out(b'  a'p')
17.  a1  :  Point
18.  c1  :  Point
19.  x'  :  Point
20.  z'  :  Point
21.  out(b  a1a)
22.  out(b  c1c)
23.  out(b'  x'a')
24.  out(b'  z'c')
25.  a1bc1  \mcong{}\msuba{}  x'b'z'
26.  a1b  \mcong{}  x'b'
27.  bc1  \mcong{}  b'z'
28.  c1a1  \mcong{}  z'x'
\mvdash{}  out(b'  x'p')


By

---

Latex:
(InstLemma  `geo-out\_transitivity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}p'\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index