---

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

∀e:BasicGeometry. ∀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 : BasicGeometry
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 : BasicGeometry
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:BasicGeometry.  \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'  \00D0  e0d'
    {}\mRightarrow{}  aa0  \00D0  e0d
    {}\mRightarrow{}  dd0  \00D0  ba
    {}\mRightarrow{}  (ba0  \00D0  e0d0  \mwedge{}  a'a0  \00D0  d'd0))


By

---

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

---

Home Index