---

Step * 2 2 2 of Lemma tarski-erect-perp-same-side


1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. c # ba
6. x : Point
7. Colinear(a;b;x)
8. ab  ⊥x cx
9. b # x
10. c1 : Point
11. c' : Point
12. p : Point
13. c=b=c1
14. c=x=c'
15. c'b ≅ cb
16. c' # c1b
17. b # cc'
18. c1=p=c'
19. ba  ⊥b pb
20. p # ba
21. d : Point
22. p-b-d
23. bd ≅ pb
24. ∃c1,c',p:Point. (((d=a=c1 ∧ d=b=c') ∧ c'a ≅ da) ∧ c' # c1a ∧ ((a # dc' ∧ c1=p=c') ∧ ab  ⊥a pa) ∧ p # ab)
⊢ ∃p,t,d:Point. (((ab ⊥ pa ∧ Colinear(a;b;t)) ∧ p-t-d) ∧ geo-tar-same-side(e;c;d;a;b))
BY
{ (ExRepD
   THEN (Assert c3 ≡ p BY
               ((InstLemma `symmetric-point-unicity` [⌜e⌝;⌜b⌝;⌜d⌝;⌜p⌝;⌜c3⌝]⋅ THENA (Auto THEN D 0 THEN Auto))
                THEN Auto
                ))
   THEN (gEliminatePoint (-1) THENA Auto)) }

1
1. e : HeytingGeometry
2. p : Point
3. a : Point
4. b : Point
5. c : Point
6. c # ba
7. x : Point
8. Colinear(a;b;x)
9. ab  ⊥x cx
10. b # x
11. c1 : Point
12. c' : Point
13. c=b=c1
14. c=x=c'
15. c'b ≅ cb
16. c' # c1b
17. b # cc'
18. c1=p=c'
19. ba  ⊥b pb
20. p # ba
21. d : Point
22. p-b-d
23. bd ≅ pb
24. c2 : Point
25. c3 : Point
26. p1 : Point
27. d=a=c2
28. d=b=p
29. pa ≅ da
30. p # c2a
31. a # dp
32. c2=p1=p
33. ab  ⊥a p1a
34. p1 # ab
35. c3 ≡ p
⊢ ∃p,t,d:Point. (((ab ⊥ pa ∧ Colinear(a;b;t)) ∧ p-t-d) ∧ geo-tar-same-side(e;c;d;a;b))

---

Latex:

---

Latex:

1.  e  :  HeytingGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  c  \#  ba
6.  x  :  Point
7.  Colinear(a;b;x)
8.  ab    \mbot{}x  cx
9.  b  \#  x
10.  c1  :  Point
11.  c'  :  Point
12.  p  :  Point
13.  c=b=c1
14.  c=x=c'
15.  c'b  \mcong{}  cb
16.  c'  \#  c1b
17.  b  \#  cc'
18.  c1=p=c'
19.  ba    \mbot{}b  pb
20.  p  \#  ba
21.  d  :  Point
22.  p-b-d
23.  bd  \mcong{}  pb
24.  \mexists{}c1,c',p:Point
          (((d=a=c1  \mwedge{}  d=b=c')  \mwedge{}  c'a  \mcong{}  da)  \mwedge{}  c'  \#  c1a  \mwedge{}  ((a  \#  dc'  \mwedge{}  c1=p=c')  \mwedge{}  ab    \mbot{}a  pa)  \mwedge{}  p  \#  ab)
\mvdash{}  \mexists{}p,t,d:Point.  (((ab  \mbot{}  pa  \mwedge{}  Colinear(a;b;t))  \mwedge{}  p-t-d)  \mwedge{}  geo-tar-same-side(e;c;d;a;b))


By

---

Latex:
(ExRepD
  THEN  (Assert  c3  \mequiv{}  p  BY
                          ((InstLemma  `symmetric-point-unicity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}c3\mkleeneclose{}]\mcdot{}
                              THENA  (Auto  THEN  D  0  THEN  Auto)
                              )
                            THEN  Auto
                            ))
  THEN  (gEliminatePoint  (-1)  THENA  Auto))

---

Home Index