---

Step * of Lemma isosceles-mid-between

∀e:HeytingGeometry. ∀a,b,c,p,q,r,x:Point.
  (a # bc ⇒ a_p_b ⇒ c_q_b ⇒ p=x=q ⇒ a=r=c ⇒ a=p=b ⇒ c=q=b ⇒ pb ≅ qb ⇒ b-x-r)
BY
{ (Auto
   THEN (∀p:hyp. FLemma `midpoint-sep` [p] 
         THEN (Auto THEN (Assert b # pq BY (InstLemma `geo-triangle-colinear` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜p⌝]⋅ THEN Auto)))
         THEN Auto)
   THEN ExRepD) }

1
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. p : Point
6. q : Point
7. r : Point
8. x : Point
9. a # bc
10. a_p_b
11. c_q_b
12. p=x=q
13. a=r=c
14. a=p=b
15. c=q=b
16. pb ≅ qb
17. c ≠ q
18. b ≠ q
19. a ≠ p
20. b ≠ p
21. a ≠ r
22. c ≠ r
23. p ≠ x
24. q ≠ x
25. b # pq
⊢ b-x-r

---

Latex:

---

Latex:
\mforall{}e:HeytingGeometry.  \mforall{}a,b,c,p,q,r,x:Point.
    (a  \#  bc  {}\mRightarrow{}  a\_p\_b  {}\mRightarrow{}  c\_q\_b  {}\mRightarrow{}  p=x=q  {}\mRightarrow{}  a=r=c  {}\mRightarrow{}  a=p=b  {}\mRightarrow{}  c=q=b  {}\mRightarrow{}  pb  \00D0  qb  {}\mRightarrow{}  b-x-r)


By

---

Latex:
(Auto
  THEN  (\mforall{}p:hyp.  FLemma  `midpoint-sep`  [p] 
              THEN  (Auto
                          THEN  (Assert  b  \#  pq  BY
                                                  (InstLemma  `geo-triangle-colinear`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THEN  Auto))
                          )
              THEN  Auto)
  THEN  ExRepD)

---

Home Index