---

Step * of Lemma eu-conga-to-cong3

∀E:EuclideanPlane. ∀a,b,c,d,e,f:Point.
  (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
{ Auto }

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

---

Latex:

---

Latex:
\mforall{}E:EuclideanPlane.  \mforall{}a,b,c,d,e,f:Point.
    (abc  =  def
    {}\mRightarrow{}  (\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:
Auto

---

Home Index