---

Step * 1 of Lemma Euclid-erect-perp-on-same-side


1. e : EuclideanPlane
2. a : Point
3. b : {b:Point| a ≠ b} 
4. c : {c:Point| Colinear(a;b;c)} 
5. q : {q:Point| q # ab} 
6. q # ab
7. q1 : Point
8. p : Point
9. [%4] : ab  ⊥c pc ∧ ab  ⊥c q1c ∧ p leftof ab ∧ q1 leftof ba
⊢ ∃p:Point [(ab  ⊥c pc ∧ p # ab ∧ (p leftof ab ⇐⇒ q leftof ab))]
BY
{ D -4 }

1
1. e : EuclideanPlane
2. a : Point
3. b : {b:Point| a ≠ b} 
4. c : {c:Point| Colinear(a;b;c)} 
5. q : {q:Point| q # ab} 
6. q leftof ab
7. q1 : Point
8. p : Point
9. [%4] : ab  ⊥c pc ∧ ab  ⊥c q1c ∧ p leftof ab ∧ q1 leftof ba
⊢ ∃p:Point [(ab  ⊥c pc ∧ p # ab ∧ (p leftof ab ⇐⇒ q leftof ab))]

2
1. e : EuclideanPlane
2. a : Point
3. b : {b:Point| a ≠ b} 
4. c : {c:Point| Colinear(a;b;c)} 
5. q : {q:Point| q # ab} 
6. q leftof ba
7. q1 : Point
8. p : Point
9. [%4] : ab  ⊥c pc ∧ ab  ⊥c q1c ∧ p leftof ab ∧ q1 leftof ba
⊢ ∃p:Point [(ab  ⊥c pc ∧ p # ab ∧ (p leftof ab ⇐⇒ q leftof ab))]

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  \{b:Point|  a  \mneq{}  b\} 
4.  c  :  \{c:Point|  Colinear(a;b;c)\} 
5.  q  :  \{q:Point|  q  \#  ab\} 
6.  q  \#  ab
7.  q1  :  Point
8.  p  :  Point
9.  [\%4]  :  ab    \mbot{}c  pc  \mwedge{}  ab    \mbot{}c  q1c  \mwedge{}  p  leftof  ab  \mwedge{}  q1  leftof  ba
\mvdash{}  \mexists{}p:Point  [(ab    \mbot{}c  pc  \mwedge{}  p  \#  ab  \mwedge{}  (p  leftof  ab  \mLeftarrow{}{}\mRightarrow{}  q  leftof  ab))]


By

---

Latex:
D  -4

---

Home Index