Step * 2 1 2 1 1 of Lemma eu-add-length-between-iff


1. EuclideanPlane
2. Point
3. Point
4. Point
5. |ac| |ab| |bc| ∈ {p:Point| O_X_p} 
6. ¬(b a ∈ Point)
7. ¬(c a ∈ Point)
8. Point
9. c_a_z ∧ az=ab
10. Point
11. z_a_x ∧ ax=ab
12. ¬a_b_c
13. ¬(b c ∈ Point)
⊢ False
BY
Assert  ⌜a_x_c⌝⋅ }

1
.....assertion..... 
1. EuclideanPlane
2. Point
3. Point
4. Point
5. |ac| |ab| |bc| ∈ {p:Point| O_X_p} 
6. ¬(b a ∈ Point)
7. ¬(c a ∈ Point)
8. Point
9. c_a_z ∧ az=ab
10. Point
11. z_a_x ∧ ax=ab
12. ¬a_b_c
13. ¬(b c ∈ Point)
⊢ a_x_c

2
1. EuclideanPlane
2. Point
3. Point
4. Point
5. |ac| |ab| |bc| ∈ {p:Point| O_X_p} 
6. ¬(b a ∈ Point)
7. ¬(c a ∈ Point)
8. Point
9. c_a_z ∧ az=ab
10. Point
11. z_a_x ∧ ax=ab
12. ¬a_b_c
13. ¬(b c ∈ Point)
14. a_x_c
⊢ False


Latex:


Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  |ac|  =  |ab|  +  |bc|
6.  \mneg{}(b  =  a)
7.  \mneg{}(c  =  a)
8.  z  :  Point
9.  c\_a\_z  \mwedge{}  az=ab
10.  x  :  Point
11.  z\_a\_x  \mwedge{}  ax=ab
12.  \mneg{}a\_b\_c
13.  \mneg{}(b  =  c)
\mvdash{}  False


By


Latex:
Assert    \mkleeneopen{}a\_x\_c\mkleeneclose{}\mcdot{}




Home Index