---

Step * of Lemma p8eu

∀e:EuclideanPlane. ∀a,b,c,x,y,z:Point.
  Cong3(abc,xyz) ⇒ (abc = xyz ∧ bac = yxz ∧ bca = yzx) supposing Triangle(a;b;c) ∧ Triangle(x;y;z)
BY
{ (Auto
   THEN (∀h:hyp. Unfolds ``eu-tri eu-cong-tri`` h  THEN ExRepD)
   THEN RepeatFor 4 ((D 0 THEN Try (Trivial) THEN Try (OnSomeHyp (\h. (ParallelNot h THEN Eq)) ⋅)))) }

1
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
⊢ ∃a',c',x',z':Point. (b_a_a' ∧ b_c_c' ∧ y_x_x' ∧ y_z_z' ∧ ba'=yx' ∧ bc'=yz' ∧ a'c'=x'z')

2
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
⊢ ∃a',c',x',z':Point. (a_b_a' ∧ a_c_c' ∧ x_y_x' ∧ x_z_z' ∧ aa'=xx' ∧ ac'=xz' ∧ a'c'=x'z')

3
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')

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,x,y,z:Point.
    Cong3(abc,xyz)  {}\mRightarrow{}  (abc  =  xyz  \mwedge{}  bac  =  yxz  \mwedge{}  bca  =  yzx)  supposing  Triangle(a;b;c)  \mwedge{}  Triangle(x;y;z)


By

---

Latex:
(Auto
  THEN  (\mforall{}h:hyp.  Unfolds  ``eu-tri  eu-cong-tri``  h    THEN  ExRepD)
  THEN  RepeatFor  4  ((D  0  THEN  Try  (Trivial)  THEN  Try  (OnSomeHyp  (\mbackslash{}h.  (ParallelNot  h  THEN  Eq))  \mcdot{}))))

---

Home Index