---

Step * of Lemma cong-angle-out-exists3

∀e:BasicGeometry. ∀a,b,c,x,y,z:Point.
  (abc ≅a xyz
  ⇒ a ≠ b
  ⇒ c ≠ b
  ⇒ x ≠ y
  ⇒ z ≠ y
  ⇒ (∃a',c',x',z':Point. ((out(b a'a) ∧ out(b c'c) ∧ out(y x'x) ∧ out(y z'z) ∧ a'bc' ≅a x'yz') ∧ Cong3(a'bc',x'yz'))))
BY
{ ((Auto THEN (Duplicate (-5) THEN D -1) THEN ExRepD)
   THEN (InstLemma `geo-between-out` [⌜e⌝;⌜b⌝;⌜a⌝;⌜a'⌝]⋅ THENA Auto)
   THEN (InstLemma `geo-between-out` [⌜e⌝;⌜b⌝;⌜c⌝;⌜c'⌝]⋅ THENA Auto)
   THEN (InstLemma `geo-between-out` [⌜e⌝;⌜y⌝;⌜x⌝;⌜x'⌝]⋅ THENA Auto)
   THEN (InstLemma `geo-between-out` [⌜e⌝;⌜y⌝;⌜z⌝;⌜z'⌝]⋅ THENA Auto)) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. abc ≅a xyz
9. a ≠ b
10. c ≠ b
11. x ≠ y
12. z ≠ y
13. a ≠ b
14. b ≠ c
15. x ≠ y
16. y ≠ z
17. a' : Point
18. c' : Point
19. x' : Point
20. z' : Point
21. b_a_a'
22. b_c_c'
23. y_x_x'
24. y_z_z'
25. ba' ≅ yx'
26. bc' ≅ yz'
27. a'c' ≅ x'z'
28. out(b aa')
29. out(b cc')
30. out(y xx')
31. out(y zz')
⊢ ∃a',c',x',z':Point. ((out(b a'a) ∧ out(b c'c) ∧ out(y x'x) ∧ out(y z'z) ∧ a'bc' ≅a x'yz') ∧ Cong3(a'bc',x'yz'))

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,x,y,z:Point.
    (abc  \mcong{}\msuba{}  xyz
    {}\mRightarrow{}  a  \mneq{}  b
    {}\mRightarrow{}  c  \mneq{}  b
    {}\mRightarrow{}  x  \mneq{}  y
    {}\mRightarrow{}  z  \mneq{}  y
    {}\mRightarrow{}  (\mexists{}a',c',x',z':Point
              ((out(b  a'a)  \mwedge{}  out(b  c'c)  \mwedge{}  out(y  x'x)  \mwedge{}  out(y  z'z)  \mwedge{}  a'bc'  \mcong{}\msuba{}  x'yz')  \mwedge{}  Cong3(a'bc',x'yz'))))


By

---

Latex:
((Auto  THEN  (Duplicate  (-5)  THEN  D  -1)  THEN  ExRepD)
  THEN  (InstLemma  `geo-between-out`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `geo-between-out`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `geo-between-out`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}x'\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `geo-between-out`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index