---

Step * 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
⊢ b-x-r
BY
{ ((InstLemma `double-pasch-exists` [⌜e⌝;⌜a⌝;⌜p⌝;⌜b⌝;⌜c⌝;⌜q⌝;⌜r⌝]⋅ THENA (Auto THEN D 0 THEN Auto))
   THEN ExRepD
   THEN RenameVar `T' (-3)) }

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


By

---

Latex:
((InstLemma  `double-pasch-exists`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  (Auto  THEN  D  0  THEN  Auto))
  THEN  ExRepD
  THEN  RenameVar  `T'  (-3))

---

Home Index