---

Step * 1 of Lemma eu-between-eq-same-side


1. e : EuclideanPlane
2. A : Point
3. B : Point
4. C : Point
5. D : Point
6. A_B_D
7. A_B_C
8. ¬(A = B ∈ Point)
9. ¬A_C_D
10. ¬A_D_C
11. ¬(A = D ∈ Point)
12. C' : Point
13. A_D_C'
14. DC'=CD
15. ¬(A = C ∈ Point)
16. D' : Point
17. A_C_D'
18. CD'=CD
19. ¬(A = C' ∈ Point)
20. B' : Point
21. A_C'_B' ∧ C'B'=CB
22. ¬(A = D' ∈ Point)
23. B'' : Point
24. A_D'_B'' ∧ D'B''=DB
⊢ False
BY
{ ((Assert ¬(B = C ∈ Point) BY
          Auto)
   THEN (Assert ¬(B = D ∈ Point) BY
               Auto)
   THEN (Assert ¬(B'' = D' ∈ Point) BY
               (ParallelLast THEN Eliminate ⌜B''⌝⋅ THEN Auto))
   THEN ...) }

1
1. e : EuclideanPlane
2. A : Point
3. B : Point
4. C : Point
5. D : Point
6. A_B_D
7. A_B_C
8. ¬(A = B ∈ Point)
9. ¬A_C_D
10. ¬A_D_C
11. ¬(A = D ∈ Point)
12. C' : Point
13. A_D_C'
14. DC'=CD
15. ¬(A = C ∈ Point)
16. D' : Point
17. A_C_D'
18. CD'=CD
19. ¬(A = C' ∈ Point)
20. B' : Point
21. A_C'_B' ∧ C'B'=CB
22. ¬(A = D' ∈ Point)
23. B'' : Point
24. A_D'_B'' ∧ D'B''=DB
25. ¬(B = C ∈ Point)
26. ¬(B = D ∈ Point)
27. ¬(B'' = D' ∈ Point)
28. BC'=B''C
⊢ False

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  A  :  Point
3.  B  :  Point
4.  C  :  Point
5.  D  :  Point
6.  A\_B\_D
7.  A\_B\_C
8.  \mneg{}(A  =  B)
9.  \mneg{}A\_C\_D
10.  \mneg{}A\_D\_C
11.  \mneg{}(A  =  D)
12.  C'  :  Point
13.  A\_D\_C'
14.  DC'=CD
15.  \mneg{}(A  =  C)
16.  D'  :  Point
17.  A\_C\_D'
18.  CD'=CD
19.  \mneg{}(A  =  C')
20.  B'  :  Point
21.  A\_C'\_B'  \mwedge{}  C'B'=CB
22.  \mneg{}(A  =  D')
23.  B''  :  Point
24.  A\_D'\_B''  \mwedge{}  D'B''=DB
\mvdash{}  False


By

---

Latex:
((Assert  \mneg{}(B  =  C)  BY
                Auto)
  THEN  (Assert  \mneg{}(B  =  D)  BY
                          Auto)
  THEN  (Assert  \mneg{}(B''  =  D')  BY
                          (ParallelLast  THEN  Eliminate  \mkleeneopen{}B''\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  (Assert  BC'=B''C  BY
                          ((Assert  B\_D\_C'  BY
                                          Auto)
                            THEN  (Assert  B''\_D'\_C  BY
                                                    Auto)
                            THEN  FLemma  `eu-three-segment`  [-1;-2]
                            THEN  Auto)))

---

Home Index