---

Step * of Lemma isosc-bisectors-between-ns

∀e:HeytingGeometry. ∀a,b,c,m,a',b',m':Point.
  (c # ab ⇒ ac ≅ bc ⇒ (c_a_a' ∧ b'_b_c) ⇒ a=m=b ⇒ a'=m'=b' ⇒ aa' ≅ bb' ⇒ c_m_m')
BY
{ (Auto THEN gSeparatedCases ⌜a'⌝⌜a⌝⋅ THEN Auto) }

1
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. m : Point
6. a' : Point
7. b' : Point
8. m' : Point
9. c # ab
10. ac ≅ bc
11. c_a_a'
12. b'_b_c
13. a=m=b
14. a'=m'=b'
15. aa' ≅ bb'
16. a' ≠ a
⊢ c_m_m'

2
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. m : Point
6. a' : Point
7. b' : Point
8. m' : Point
9. c # ab
10. ac ≅ bc
11. c_a_a
12. b'_b_c
13. a=m=b
14. a=m'=b'
15. aa ≅ bb'
16. a' ≡ a
⊢ c_m_m'

---

Latex:

---

Latex:
\mforall{}e:HeytingGeometry.  \mforall{}a,b,c,m,a',b',m':Point.
    (c  \#  ab  {}\mRightarrow{}  ac  \00D0  bc  {}\mRightarrow{}  (c\_a\_a'  \mwedge{}  b'\_b\_c)  {}\mRightarrow{}  a=m=b  {}\mRightarrow{}  a'=m'=b'  {}\mRightarrow{}  aa'  \00D0  bb'  {}\mRightarrow{}  c\_m\_m')


By

---

Latex:
(Auto  THEN  gSeparatedCases  \mkleeneopen{}a'\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index