---

Step * 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. [%8] : xx1  ⊥x px ∧ xx1  ⊥x qx ∧ p leftof xx1 ∧ q leftof x1x
⊢ ∃m:Line. (x I m ∧ x1 # m)
BY
{ ((Assert xx1  ⊥x px ∧ xx1  ⊥x qx ∧ p leftof xx1 ∧ q leftof x1x BY
          (Auto THEN Unhide THEN Auto THEN (Unfold `geo-perp-in` 0 THEN Auto) THEN Unfold `right-angle` 0 THEN Auto))
   THEN Thin (-2)
   ) }

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
⊢ ∃m:Line. (x I m ∧ x1 # m)

---

Latex:

---

Latex:

1.  e  :  EuclideanParPlane
2.  x  :  Point
3.  x1  :  Point
4.  x  \mneq{}  x1
5.  q  :  Point
6.  p  :  Point
7.  [\%8]  :  xx1    \mbot{}x  px  \mwedge{}  xx1    \mbot{}x  qx  \mwedge{}  p  leftof  xx1  \mwedge{}  q  leftof  x1x
\mvdash{}  \mexists{}m:Line.  (x  I  m  \mwedge{}  x1  \#  m)


By

---

Latex:
((Assert  xx1    \mbot{}x  px  \mwedge{}  xx1    \mbot{}x  qx  \mwedge{}  p  leftof  xx1  \mwedge{}  q  leftof  x1x  BY
                (Auto
                  THEN  Unhide
                  THEN  Auto
                  THEN  (Unfold  `geo-perp-in`  0  THEN  Auto)
                  THEN  Unfold  `right-angle`  0
                  THEN  Auto))
  THEN  Thin  (-2)
  )

---

Home Index