---

Step * 1 of Lemma eu-conga-to-cong3


1. E : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. abc = def
⊢ ∃a',c',d',f':Point. (out(b a'a) ∧ out(b cc') ∧ out(e d'd) ∧ out(e ff') ∧ Cong3(a'bc',d'ef'))
BY
{ Unfold `eu-cong-angle` 8 }

1
1. E : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. (¬(a = b ∈ Point))
∧ (¬(c = b ∈ Point))
∧ (¬(d = e ∈ Point))
∧ (¬(f = e ∈ Point))
∧ (∃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'))
⊢ ∃a',c',d',f':Point. (out(b a'a) ∧ out(b cc') ∧ out(e d'd) ∧ out(e ff') ∧ Cong3(a'bc',d'ef'))

---

Latex:

---

Latex:

1.  E  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  e  :  Point
7.  f  :  Point
8.  abc  =  def
\mvdash{}  \mexists{}a',c',d',f':Point.  (out(b  a'a)  \mwedge{}  out(b  cc')  \mwedge{}  out(e  d'd)  \mwedge{}  out(e  ff')  \mwedge{}  Cong3(a'bc',d'ef'))


By

---

Latex:
Unfold  `eu-cong-angle`  8

---

Home Index