---

Step * 1 1 of Lemma proj-point-sep_defA

.....assertion..... 
1. e : EuclideanParPlane
2. x : Point
3. x1 : Point
4. x ≠ x1
⊢ ∃m:Line. (x I m ∧ x1 # m)
BY
{ ((InstLemma `Euclid-erect-2perp` [⌜e⌝;⌜x⌝;⌜x1⌝;⌜x⌝]⋅ THENA Auto) THEN RepeatFor 2 (D -1)) }

1
1. e : EuclideanParPlane
2. x : Point
3. x1 : Point
4. x ≠ x1
5. q : Point
6. p : Point
7. [%8] : xx1  ⊥x px ∧ xx1  ⊥x qx ∧ p leftof xx1 ∧ q leftof x1x
⊢ ∃m:Line. (x I m ∧ x1 # m)

---

Latex:

---

Latex:
.....assertion..... 
1.  e  :  EuclideanParPlane
2.  x  :  Point
3.  x1  :  Point
4.  x  \mneq{}  x1
\mvdash{}  \mexists{}m:Line.  (x  I  m  \mwedge{}  x1  \#  m)


By

---

Latex:
((InstLemma  `Euclid-erect-2perp`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  RepeatFor  2  (D  -1))

---

Home Index