---

Step * of Lemma cong-angle-out-aux_1

∀g:BasicGeometry. ∀a,b,c,d,e,f,a',c',d',f':Point.
  (abc ≅a def ⇒ out(b a'a) ⇒ out(b c'c) ⇒ out(e d'd) ⇒ out(e f'f) ⇒ ba' ≅ ed' ⇒ bc' ≅ ef' ⇒ a'c' ≅ d'f')
BY
{ ((Auto THEN D 12 THEN ExRepD)
   THEN (Assert out(b a1a') BY
               ((Assert out(b aa1) BY
                       (InstLemma `geo-between-out` [⌜g⌝;⌜b⌝;⌜a⌝;⌜a1⌝]⋅ THEN Auto))
                THEN InstLemma `geo-out_transitivity` [⌜g⌝;⌜b⌝;⌜a'⌝;⌜a⌝;⌜a1⌝]⋅
                THEN EAuto 1))
   ) }

1
1. g : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. a' : Point
9. c' : Point
10. d' : Point
11. f' : Point
12. a ≠ b
13. b ≠ c
14. d ≠ e
15. e ≠ f
16. a1 : Point
17. c1 : Point
18. x' : Point
19. z' : Point
20. b_a_a1
21. b_c_c1
22. e_d_x'
23. e_f_z'
24. ba1 ≅ ex'
25. bc1 ≅ ez'
26. a1c1 ≅ x'z'
27. out(b a'a)
28. out(b c'c)
29. out(e d'd)
30. out(e f'f)
31. ba' ≅ ed'
32. bc' ≅ ef'
33. out(b a1a')
⊢ a'c' ≅ d'f'

---

Latex:

---

Latex:
\mforall{}g:BasicGeometry.  \mforall{}a,b,c,d,e,f,a',c',d',f':Point.
    (abc  \mcong{}\msuba{}  def
    {}\mRightarrow{}  out(b  a'a)
    {}\mRightarrow{}  out(b  c'c)
    {}\mRightarrow{}  out(e  d'd)
    {}\mRightarrow{}  out(e  f'f)
    {}\mRightarrow{}  ba'  \mcong{}  ed'
    {}\mRightarrow{}  bc'  \mcong{}  ef'
    {}\mRightarrow{}  a'c'  \mcong{}  d'f')


By

---

Latex:
((Auto  THEN  D  12  THEN  ExRepD)
  THEN  (Assert  out(b  a1a')  BY
                          ((Assert  out(b  aa1)  BY
                                          (InstLemma  `geo-between-out`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{}]\mcdot{}  THEN  Auto))
                            THEN  InstLemma  `geo-out\_transitivity`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{}]\mcdot{}
                            THEN  EAuto  1))
  )

---

Home Index