---

Step * 1 3 1 of Lemma not-not-inner-pasch


1. e : EuclideanPlane
2. b : Point
3. a : Point
4. c : Point
5. p : Point
6. a_p_b
7. q : Point
8. b_q_b
9. ∀X:ℙ
     (Stable{X}
     ⇒ (((¬(a = b ∈ Point)) ∧ (b = a ∈ Point)) ⇒ X)
     ⇒ (((¬(a = b ∈ Point)) ∧ (b = b ∈ Point)) ⇒ X)
     ⇒ (((¬(a = b ∈ Point)) ∧ b-a-b) ⇒ X)
     ⇒ (((¬(a = b ∈ Point)) ∧ a-b-b) ⇒ X)
     ⇒ (((¬(a = b ∈ Point)) ∧ a-b-b) ⇒ X)
     ⇒ ((¬Colinear(a;b;b)) ⇒ X)
     ⇒ X)
10. ¬(a = b ∈ Point)
11. c = b ∈ Point
12. b = q ∈ Point
⊢ ¬¬(∃x:Point. (p_x_b ∧ b_x_a))
BY
{ ((D 0 THENA Auto) THEN D -1 THEN With ⌜b⌝ (D 0)⋅ THEN EAuto 1) }

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  b  :  Point
3.  a  :  Point
4.  c  :  Point
5.  p  :  Point
6.  a\_p\_b
7.  q  :  Point
8.  b\_q\_b
9.  \mforall{}X:\mBbbP{}
          (Stable\{X\}
          {}\mRightarrow{}  (((\mneg{}(a  =  b))  \mwedge{}  (b  =  a))  {}\mRightarrow{}  X)
          {}\mRightarrow{}  (((\mneg{}(a  =  b))  \mwedge{}  (b  =  b))  {}\mRightarrow{}  X)
          {}\mRightarrow{}  (((\mneg{}(a  =  b))  \mwedge{}  b-a-b)  {}\mRightarrow{}  X)
          {}\mRightarrow{}  (((\mneg{}(a  =  b))  \mwedge{}  a-b-b)  {}\mRightarrow{}  X)
          {}\mRightarrow{}  (((\mneg{}(a  =  b))  \mwedge{}  a-b-b)  {}\mRightarrow{}  X)
          {}\mRightarrow{}  ((\mneg{}Colinear(a;b;b))  {}\mRightarrow{}  X)
          {}\mRightarrow{}  X)
10.  \mneg{}(a  =  b)
11.  c  =  b
12.  b  =  q
\mvdash{}  \mneg{}\mneg{}(\mexists{}x:Point.  (p\_x\_b  \mwedge{}  b\_x\_a))


By

---

Latex:
((D  0  THENA  Auto)  THEN  D  -1  THEN  With  \mkleeneopen{}b\mkleeneclose{}  (D  0)\mcdot{}  THEN  EAuto  1)

---

Home Index