---

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

∀e:EuclideanPlane. ∀b,a,a',a0,e0,d,d',d0:Point.
  (out(b aa') ⇒ out(e0 dd') ⇒ b_a_a0 ⇒ e0_d_d0 ⇒ ba'=e0d' ⇒ aa0=e0d ⇒ dd0=ba ⇒ (ba0=e0d0 ∧ a'a0=d'd0))
BY
{ RepeatFor 17 ((D 0 THENA Auto)) }

1
1. e : EuclideanPlane
2. b : Point
3. a : Point
4. a' : Point
5. a0 : Point
6. e0 : Point
7. d : Point
8. d' : Point
9. d0 : Point
10. out(b aa')
11. out(e0 dd')
12. b_a_a0
13. e0_d_d0
14. ba'=e0d'
15. aa0=e0d
16. dd0=ba
⊢ ba0=e0d0

2
1. e : EuclideanPlane
2. b : Point
3. a : Point
4. a' : Point
5. a0 : Point
6. e0 : Point
7. d : Point
8. d' : Point
9. d0 : Point
10. out(b aa')
11. out(e0 dd')
12. b_a_a0
13. e0_d_d0
14. ba'=e0d'
15. aa0=e0d
16. dd0=ba
⊢ a'a0=d'd0

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}b,a,a',a0,e0,d,d',d0:Point.
    (out(b  aa')
    {}\mRightarrow{}  out(e0  dd')
    {}\mRightarrow{}  b\_a\_a0
    {}\mRightarrow{}  e0\_d\_d0
    {}\mRightarrow{}  ba'=e0d'
    {}\mRightarrow{}  aa0=e0d
    {}\mRightarrow{}  dd0=ba
    {}\mRightarrow{}  (ba0=e0d0  \mwedge{}  a'a0=d'd0))


By

---

Latex:
RepeatFor  17  ((D  0  THENA  Auto))

---

Home Index