---

Step * of Lemma cong-angle-out-aux-weak

∀g:HeytingGeometry. ∀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⌝]⋅ THENA Auto)
                 )
                THEN EAuto 1
                ))
   ) }

1
1. g : HeytingGeometry
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:HeytingGeometry.  \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{}  THENA  Auto)
                              )
                            THEN  EAuto  1
                            ))
  )

---

Home Index