---

Step * of Lemma isosc-bisectors-between_1-ns

∀e:HeytingGeometry. ∀a,b,c,m,a',b',m':Point.
  (c # a'b' ⇒ ac ≅ bc ⇒ (c_a'_a ∧ c_b'_b) ⇒ 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 # a'b'
10. ac ≅ bc
11. c_a'_a
12. c_b'_b
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. c_b'_b
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  \#  a'b'  {}\mRightarrow{}  ac  \00D0  bc  {}\mRightarrow{}  (c\_a'\_a  \mwedge{}  c\_b'\_b)  {}\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