---

Step * 1 of Lemma geo-between-lt-angle


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. p : Point
6. a # bc
7. b-p-c
⊢ (¬out(a bc))
∧ (∃p@0,p',x',z':Point. (bap ≅a bap@0 ∧ a_p'_p@0 ∧ (out(a bx') ∧ out(a cz')) ∧ (¬b_a_p@0) ∧ x'_p'_z' ∧ p' ≠ z'))
BY
{ ((InstLemma `Euclid-midpoint-1` [⌜e⌝;⌜p⌝;⌜c⌝]⋅ THEN Auto) THEN ExRepD) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. p : Point
6. a # bc
7. b-p-c
8. d : Point
9. p=d=c
⊢ ¬out(a bc)

2
.....wf..... 
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. p : Point
6. a # bc
7. b-p-c
8. d : Point
9. p=d=c
⊢ istype(out(a bc))

3
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. p : Point
6. a # bc
7. b-p-c
8. d : Point
9. p=d=c
10. ¬out(a bc)
⊢ ∃p@0,p',x',z':Point. (bap ≅a bap@0 ∧ a_p'_p@0 ∧ (out(a bx') ∧ out(a cz')) ∧ (¬b_a_p@0) ∧ x'_p'_z' ∧ p' ≠ z')

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  p  :  Point
6.  a  \#  bc
7.  b-p-c
\mvdash{}  (\mneg{}out(a  bc))
\mwedge{}  (\mexists{}p@0,p',x',z':Point
        (bap  \mcong{}\msuba{}  bap@0  \mwedge{}  a\_p'\_p@0  \mwedge{}  (out(a  bx')  \mwedge{}  out(a  cz'))  \mwedge{}  (\mneg{}b\_a\_p@0)  \mwedge{}  x'\_p'\_z'  \mwedge{}  p'  \mneq{}  z'))


By

---

Latex:
((InstLemma  `Euclid-midpoint-1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  ExRepD)

---

Home Index