---

Step * 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
⊢ b-x-r
BY
{ (Assert pr ≅ qr BY
         ((InstLemma `geo-inner-five-segment` [⌜e⌝;⌜b⌝;⌜p⌝;⌜a⌝;⌜r⌝;⌜b⌝;⌜q⌝;⌜c⌝;⌜r⌝] ⋅ THEN Auto)
          THENA (((D 14 THEN D 16) THEN D 13) THEN Auto)
          )) }

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
26. T : Point
27. r-T-b
28. p-T-q
29. pr ≅ qr
⊢ b-x-r

---

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
\mvdash{}  b-x-r


By

---

Latex:
(Assert  pr  \00D0  qr  BY
              ((InstLemma  `geo-inner-five-segment`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{}]  \mcdot{}  THEN  Auto)
                THENA  (((D  14  THEN  D  16)  THEN  D  13)  THEN  Auto)
                ))

---

Home Index