---

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


1. e : EuclideanPlane
2. B' : Point
3. A : Point
4. B : Point
5. C : Point
6. D : Point
7. A_B_D
8. A_B_C
9. ¬(A = B ∈ Point)
10. ¬A_C_D
11. ¬A_D_C
12. ¬(A = D ∈ Point)
13. C' : Point
14. A_D_C'
15. DC'=CD
16. ¬(A = C ∈ Point)
17. D' : Point
18. A_C_D'
19. CD'=CD
20. ¬(A = C' ∈ Point)
21. A_C'_B'
22. C'B'=CB
23. ¬(A = D' ∈ Point)
24. A_D'_B'
25. D'B'=DB
26. ¬(B = C ∈ Point)
27. ¬(B = D ∈ Point)
28. ¬(B' = D' ∈ Point)
29. BC'=B'C
30. D'C'=DC
31. E : Point
32. C_E_C'
33. D_E_D'
⊢ False
BY
{ ((Assert EC=EC' BY
          (Using [`C', ⌜D⌝ ; `A', ⌜D'⌝ ; `c', ⌜D⌝; `a', ⌜D'⌝ ] (BLemma `eu-inner-five-segment`) ⋅ THEN Auto))
   THEN (Assert ED=ED' BY
               (Using [`C', ⌜C⌝ ; `A', ⌜C'⌝ ; `c', ⌜C⌝; `a', ⌜C'⌝ ] (BLemma `eu-inner-five-segment`) ⋅ THEN Auto))
   ) }

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

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  B'  :  Point
3.  A  :  Point
4.  B  :  Point
5.  C  :  Point
6.  D  :  Point
7.  A\_B\_D
8.  A\_B\_C
9.  \mneg{}(A  =  B)
10.  \mneg{}A\_C\_D
11.  \mneg{}A\_D\_C
12.  \mneg{}(A  =  D)
13.  C'  :  Point
14.  A\_D\_C'
15.  DC'=CD
16.  \mneg{}(A  =  C)
17.  D'  :  Point
18.  A\_C\_D'
19.  CD'=CD
20.  \mneg{}(A  =  C')
21.  A\_C'\_B'
22.  C'B'=CB
23.  \mneg{}(A  =  D')
24.  A\_D'\_B'
25.  D'B'=DB
26.  \mneg{}(B  =  C)
27.  \mneg{}(B  =  D)
28.  \mneg{}(B'  =  D')
29.  BC'=B'C
30.  D'C'=DC
31.  E  :  Point
32.  C\_E\_C'
33.  D\_E\_D'
\mvdash{}  False


By

---

Latex:
((Assert  EC=EC'  BY
                (Using  [`C',  \mkleeneopen{}D\mkleeneclose{}  ;  `A',  \mkleeneopen{}D'\mkleeneclose{}  ;  `c',  \mkleeneopen{}D\mkleeneclose{};  `a',  \mkleeneopen{}D'\mkleeneclose{}  ]  (BLemma  `eu-inner-five-segment`)  \mcdot{}
                  THEN  Auto
                  ))
  THEN  (Assert  ED=ED'  BY
                          (Using  [`C',  \mkleeneopen{}C\mkleeneclose{}  ;  `A',  \mkleeneopen{}C'\mkleeneclose{}  ;  `c',  \mkleeneopen{}C\mkleeneclose{};  `a',  \mkleeneopen{}C'\mkleeneclose{}  ]  (BLemma  `eu-inner-five-segment`)  \mcdot{}
                            THEN  Auto
                            ))
  )

---

Home Index