---

Step * 3 of Lemma p8eu


1. e : EuclideanPlane@i'
2. a : Point@i
3. b : Point@i
4. c : Point@i
5. x : Point@i
6. y : Point@i
7. z : Point@i
8. ¬(a = b ∈ Point)
9. ¬(a = c ∈ Point)
10. ¬(b = c ∈ Point)
11. ¬(x = y ∈ Point)
12. ¬(x = z ∈ Point)
13. ¬(y = z ∈ Point)
14. ab=xy@i
15. bc=yz@i
16. ca=zx@i
17. abc = xyz
18. bac = yxz
⊢ ∃a',c',x',z':Point. (c_b_a' ∧ c_a_c' ∧ z_y_x' ∧ z_x_z' ∧ ca'=zx' ∧ cc'=zz' ∧ a'c'=x'z')
BY
{ (InstConcl [⌜b⌝;⌜a⌝;⌜y⌝;⌜x⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane@i'
2.  a  :  Point@i
3.  b  :  Point@i
4.  c  :  Point@i
5.  x  :  Point@i
6.  y  :  Point@i
7.  z  :  Point@i
8.  \mneg{}(a  =  b)
9.  \mneg{}(a  =  c)
10.  \mneg{}(b  =  c)
11.  \mneg{}(x  =  y)
12.  \mneg{}(x  =  z)
13.  \mneg{}(y  =  z)
14.  ab=xy@i
15.  bc=yz@i
16.  ca=zx@i
17.  abc  =  xyz
18.  bac  =  yxz
\mvdash{}  \mexists{}a',c',x',z':Point.  (c\_b\_a'  \mwedge{}  c\_a\_c'  \mwedge{}  z\_y\_x'  \mwedge{}  z\_x\_z'  \mwedge{}  ca'=zx'  \mwedge{}  cc'=zz'  \mwedge{}  a'c'=x'z')


By

---

Latex:
(InstConcl  [\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index