---

Step * of Lemma cong-angle-out-aux2

∀g:HeytingGeometry. ∀a,b,c,d,e,f,a',c',d',f':Point.
  ((a # bc ∧ a'c' ≅ d'f')
  ⇒ d # ef
  ⇒ out(b a'a)
  ⇒ out(b c'c)
  ⇒ out(e d'd)
  ⇒ out(e f'f)
  ⇒ ba' ≅ ed'
  ⇒ bc' ≅ ef'
  ⇒ abc ≅a def)
BY
{ (Auto THEN (D 0 THENL [Auto; Id])) }

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'c' ≅ d'f'
14. d # ef
15. out(b a'a)
16. out(b c'c)
17. out(e d'd)
18. out(e f'f)
19. ba' ≅ ed'
20. bc' ≅ ef'
⊢ ∃a',c',x',z':Point. (b_a_a' ∧ b_c_c' ∧ e_d_x' ∧ e_f_z' ∧ ba' ≅ ex' ∧ bc' ≅ ez' ∧ a'c' ≅ x'z')

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (D  0  THENL  [Auto;  Id]))

---

Home Index