---

Step * of Lemma cong-angle-out-aux

∀g:HeytingGeometry. ∀a,b,c,d,e,f,a',c',d',f':Point.
  ((a # bc ∧ abc ≅a def)
  ⇒ d # ef
  ⇒ 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 13 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 # bc
13. a ≠ b
14. b ≠ c
15. d ≠ e
16. e ≠ f
17. a1 : Point
18. c1 : Point
19. x' : Point
20. z' : Point
21. b_a_a1
22. b_c_c1
23. e_d_x'
24. e_f_z'
25. ba1 ≅ ex'
26. bc1 ≅ ez'
27. a1c1 ≅ x'z'
28. d # ef
29. out(b a'a)
30. out(b c'c)
31. out(e d'd)
32. out(e f'f)
33. ba' ≅ ed'
34. bc' ≅ ef'
35. out(b a1a')
⊢ a'c' ≅ d'f'

---

Latex:

---

Latex:
\mforall{}g:HeytingGeometry.  \mforall{}a,b,c,d,e,f,a',c',d',f':Point.
    ((a  \#  bc  \mwedge{}  abc  \mcong{}\msuba{}  def)
    {}\mRightarrow{}  d  \#  ef
    {}\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  13  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