---

Step * of Lemma isosceles-mid-cong-angles

∀e:HeytingGeometry. ∀a,b,c,m:Point.  (c # ab ⇒ a=m=b ⇒ ac ≅ bc ⇒ acm ≅a bcm)
BY
{ (Auto
   THEN Unfold `geo-cong-angle` 0
   THEN (D 0 THENL [Auto; ((((InstConcl [⌜a⌝;⌜m⌝;⌜b⌝;⌜m⌝]⋅ THENA Auto) THEN GenRepD) THEN Auto) THEN D 7 THEN Auto)])) }

1
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. m : Point
6. c # ab
7. a=m=b
8. ac ≅ bc
9. a ≠ c
⊢ c ≠ m

---

Latex:

---

Latex:
\mforall{}e:HeytingGeometry.  \mforall{}a,b,c,m:Point.    (c  \#  ab  {}\mRightarrow{}  a=m=b  {}\mRightarrow{}  ac  \mcong{}  bc  {}\mRightarrow{}  acm  \mcong{}\msuba{}  bcm)


By

---

Latex:
(Auto
  THEN  Unfold  `geo-cong-angle`  0
  THEN  (D  0
              THENL  [Auto
                          ;  ((((InstConcl  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  GenRepD)  THEN  Auto)
                                THEN  D  7
                                THEN  Auto)]
  ))

---

Home Index