---

Step * of Lemma out-preserves-angle-cong_1

∀e:BasicGeometry. ∀a,b,c,a',b',c',p,q,p',q':Point.
  (abc ≅a a'b'c' ⇒ out(b cq) ⇒ out(b ap) ⇒ out(b' c'q') ⇒ out(b' a'p') ⇒ pbq ≅a p'b'q')
BY
{ ((Auto THEN (FLemma `cong-angle-out-exists3` [12] THENA Auto)) THEN ExRepD) }

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. Cong3(a1bc1,x'b'z')
⊢ pbq ≅a p'b'q'

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,a',b',c',p,q,p',q':Point.
    (abc  \mcong{}\msuba{}  a'b'c'  {}\mRightarrow{}  out(b  cq)  {}\mRightarrow{}  out(b  ap)  {}\mRightarrow{}  out(b'  c'q')  {}\mRightarrow{}  out(b'  a'p')  {}\mRightarrow{}  pbq  \mcong{}\msuba{}  p'b'q')


By

---

Latex:
((Auto  THEN  (FLemma  `cong-angle-out-exists3`  [12]  THENA  Auto))  THEN  ExRepD)

---

Home Index