Step
*
1
2
1
of Lemma
not-not-inner-pasch
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. p : Point
6. a_p_a
7. q : Point
8. b_q_a
9. ∀X:ℙ
(Stable{X}
⇒ (((¬(a = b ∈ Point)) ∧ (a = a ∈ Point))
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ (a = b ∈ Point))
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ a-a-b)
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ a-a-b)
⇒ X)
⇒ (((¬(a = b ∈ Point)) ∧ a-b-a)
⇒ X)
⇒ ((¬Colinear(a;b;a))
⇒ X)
⇒ X)
10. ¬(a = b ∈ Point)
11. c = a ∈ Point
12. a = p ∈ Point
⊢ ¬¬(∃x:Point. (a_x_b ∧ q_x_a))
BY
{ ((D 0 THENA Auto) THEN D -1 THEN With ⌜q⌝ (D 0)⋅ THEN EAuto 1) }
Latex:
Latex:
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. p : Point
6. a\_p\_a
7. q : Point
8. b\_q\_a
9. \mforall{}X:\mBbbP{}
(Stable\{X\}
{}\mRightarrow{} (((\mneg{}(a = b)) \mwedge{} (a = a)) {}\mRightarrow{} X)
{}\mRightarrow{} (((\mneg{}(a = b)) \mwedge{} (a = b)) {}\mRightarrow{} X)
{}\mRightarrow{} (((\mneg{}(a = b)) \mwedge{} a-a-b) {}\mRightarrow{} X)
{}\mRightarrow{} (((\mneg{}(a = b)) \mwedge{} a-a-b) {}\mRightarrow{} X)
{}\mRightarrow{} (((\mneg{}(a = b)) \mwedge{} a-b-a) {}\mRightarrow{} X)
{}\mRightarrow{} ((\mneg{}Colinear(a;b;a)) {}\mRightarrow{} X)
{}\mRightarrow{} X)
10. \mneg{}(a = b)
11. c = a
12. a = p
\mvdash{} \mneg{}\mneg{}(\mexists{}x:Point. (a\_x\_b \mwedge{} q\_x\_a))
By
Latex:
((D 0 THENA Auto) THEN D -1 THEN With \mkleeneopen{}q\mkleeneclose{} (D 0)\mcdot{} THEN EAuto 1)
Home
Index