---

Step * 1 1 1 1 1 of Lemma proj-point-sep_defA


1. e : EuclideanParPlane
2. x : Point
3. x1 : Point
4. x ≠ x1
5. q : Point
6. p : Point
7. xx1  ⊥x px ∧ xx1  ⊥x qx ∧ p leftof xx1 ∧ q leftof x1x
8. l : Line
9. x ≡ fst(l) ∧ p ≡ fst(snd(l))
⊢ x I l ∧ x1 # l
BY
{ D 0 }

1
1. e : EuclideanParPlane
2. x : Point
3. x1 : Point
4. x ≠ x1
5. q : Point
6. p : Point
7. xx1  ⊥x px ∧ xx1  ⊥x qx ∧ p leftof xx1 ∧ q leftof x1x
8. l : Line
9. x ≡ fst(l) ∧ p ≡ fst(snd(l))
⊢ x I l

2
1. e : EuclideanParPlane
2. x : Point
3. x1 : Point
4. x ≠ x1
5. q : Point
6. p : Point
7. xx1  ⊥x px ∧ xx1  ⊥x qx ∧ p leftof xx1 ∧ q leftof x1x
8. l : Line
9. x ≡ fst(l) ∧ p ≡ fst(snd(l))
⊢ x1 # l

---

Latex:

---

Latex:

1.  e  :  EuclideanParPlane
2.  x  :  Point
3.  x1  :  Point
4.  x  \mneq{}  x1
5.  q  :  Point
6.  p  :  Point
7.  xx1    \mbot{}x  px  \mwedge{}  xx1    \mbot{}x  qx  \mwedge{}  p  leftof  xx1  \mwedge{}  q  leftof  x1x
8.  l  :  Line
9.  x  \mequiv{}  fst(l)  \mwedge{}  p  \mequiv{}  fst(snd(l))
\mvdash{}  x  I  l  \mwedge{}  x1  \#  l


By

---

Latex:
D  0

---

Home Index