---

Step * of Lemma geo-between-cong-tri-exists

∀[e:BasicGeometry]. ∀[a,b,c,a',c':Point].
  (a_b_c ⇒ ac ≅ a'c' ⇒ (¬¬(∃b':Point. (Cong3(abc,a'b'c') ∧ Colinear(a';b';c')))))
BY
{ Auto }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. c' : Point
7. a_b_c
8. ac ≅ a'c'
⊢ ¬¬(∃b':Point. (Cong3(abc,a'b'c') ∧ Colinear(a';b';c')))

---

Latex:

---

Latex:
\mforall{}[e:BasicGeometry].  \mforall{}[a,b,c,a',c':Point].
    (a\_b\_c  {}\mRightarrow{}  ac  \00D0  a'c'  {}\mRightarrow{}  (\mneg{}\mneg{}(\mexists{}b':Point.  (Cong3(abc,a'b'c')  \mwedge{}  Colinear(a';b';c')))))


By

---

Latex:
Auto

---

Home Index