---

Step * 1 1 1 1 of Lemma isosceles-mid-between


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
26. T : Point
27. r-T-b
28. p-T-q
29. pr ≅ qr
30. Tp ≅ Tq
⊢ b-x-r
BY
{ (((Assert p=T=q BY
           (D 0 THEN Auto))
    THEN (Assert T ≡ x BY
                (InstLemma `at-most-one-midpoint` [⌜e⌝;⌜p⌝;⌜q⌝;⌜T⌝;⌜x⌝]⋅ THEN Auto))
    )
   THEN gEliminatePoint (-1)
   THEN Auto) }

---

Latex:

---

Latex:

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  \00D0  qb
17.  c  \mneq{}  q
18.  b  \mneq{}  q
19.  a  \mneq{}  p
20.  b  \mneq{}  p
21.  a  \mneq{}  r
22.  c  \mneq{}  r
23.  p  \mneq{}  x
24.  q  \mneq{}  x
25.  b  \#  pq
26.  T  :  Point
27.  r-T-b
28.  p-T-q
29.  pr  \00D0  qr
30.  Tp  \00D0  Tq
\mvdash{}  b-x-r


By

---

Latex:
(((Assert  p=T=q  BY
                  (D  0  THEN  Auto))
    THEN  (Assert  T  \mequiv{}  x  BY
                            (InstLemma  `at-most-one-midpoint`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto))
    )
  THEN  gEliminatePoint  (-1)
  THEN  Auto)

---

Home Index