---

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


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. p : Point
6. q : Point
7. b_q_c
8. ∀X:ℙ
     (Stable{X}
     ⇒ (((¬(a = b ∈ Point)) ∧ (c = a ∈ Point)) ⇒ X)
     ⇒ (((¬(a = b ∈ Point)) ∧ (c = b ∈ Point)) ⇒ X)
     ⇒ (((¬(a = b ∈ Point)) ∧ c-a-b) ⇒ X)
     ⇒ (((¬(a = b ∈ Point)) ∧ a-c-b) ⇒ X)
     ⇒ (((¬(a = b ∈ Point)) ∧ a-b-c) ⇒ X)
     ⇒ ((¬Colinear(a;b;c)) ⇒ X)
     ⇒ X)
9. ¬Colinear(a;b;c)
10. a-p-c
⊢ ∃x:Point. (p_x_b ∧ q_x_a)
BY
{ (InstLemma `eu-inner-pasch-property` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜p⌝;⌜q⌝]⋅ THENA Auto) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. p : Point
6. q : Point
7. b_q_c
8. ∀X:ℙ
     (Stable{X}
     ⇒ (((¬(a = b ∈ Point)) ∧ (c = a ∈ Point)) ⇒ X)
     ⇒ (((¬(a = b ∈ Point)) ∧ (c = b ∈ Point)) ⇒ X)
     ⇒ (((¬(a = b ∈ Point)) ∧ c-a-b) ⇒ X)
     ⇒ (((¬(a = b ∈ Point)) ∧ a-c-b) ⇒ X)
     ⇒ (((¬(a = b ∈ Point)) ∧ a-b-c) ⇒ X)
     ⇒ ((¬Colinear(a;b;c)) ⇒ X)
     ⇒ X)
9. ¬Colinear(a;b;c)
10. a-p-c
11. p-eu-inner-pasch(e;a;b;c;p;q)-b ∧ q-eu-inner-pasch(e;a;b;c;p;q)-a
⊢ ∃x:Point. (p_x_b ∧ q_x_a)

---

Latex:

---

Latex:

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


By

---

Latex:
(InstLemma  `eu-inner-pasch-property`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index