---

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

∀e:EuclideanPlane. ∀[A,B,C,D:Point].  (¬((¬A_C_D) ∧ (¬A_D_C))) supposing ((¬(A = B ∈ Point)) and A_B_C and A_B_D)
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN ((Assert ¬(A = D ∈ Point) BY
                (NotEqualFromEuBetween⋅ THEN Auto))
         THEN (Prolong ⌜A⌝ ⌜D⌝ `C\'' ⌜C⌝ ⌜D⌝⋅ THENA Auto)
         )
   THEN (Assert ¬(A = C ∈ Point) BY
               (NotEqualFromEuBetween⋅ THEN Auto))
   THEN (Prolong ⌜A⌝ ⌜C⌝ `D\'' ⌜C⌝ ⌜D⌝⋅ THENA Auto)
   THEN ExRepD
   THEN (Assert ¬(A = C' ∈ Point) BY
               (NotEqualFromEuBetween⋅ THEN Auto))
   THEN (Prolong ⌜A⌝ ⌜C'⌝ `B\'' ⌜C⌝ ⌜B⌝⋅ THENA Auto)
   THEN (Assert ¬(A = D' ∈ Point) BY
               (NotEqualFromEuBetween⋅ THEN Auto))
   THEN (Prolong ⌜A⌝ ⌜D'⌝ `B\'\'' ⌜D⌝ ⌜B⌝⋅ THENA Auto)) }

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
⊢ False

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane
    \mforall{}[A,B,C,D:Point].    (\mneg{}((\mneg{}A\_C\_D)  \mwedge{}  (\mneg{}A\_D\_C)))  supposing  ((\mneg{}(A  =  B))  and  A\_B\_C  and  A\_B\_D)


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  ((Assert  \mneg{}(A  =  D)  BY
                            (NotEqualFromEuBetween\mcdot{}  THEN  Auto))
              THEN  (Prolong  \mkleeneopen{}A\mkleeneclose{}  \mkleeneopen{}D\mkleeneclose{}  `C\mbackslash{}''  \mkleeneopen{}C\mkleeneclose{}  \mkleeneopen{}D\mkleeneclose{}\mcdot{}  THENA  Auto)
              )
  THEN  (Assert  \mneg{}(A  =  C)  BY
                          (NotEqualFromEuBetween\mcdot{}  THEN  Auto))
  THEN  (Prolong  \mkleeneopen{}A\mkleeneclose{}  \mkleeneopen{}C\mkleeneclose{}  `D\mbackslash{}''  \mkleeneopen{}C\mkleeneclose{}  \mkleeneopen{}D\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (Assert  \mneg{}(A  =  C')  BY
                          (NotEqualFromEuBetween\mcdot{}  THEN  Auto))
  THEN  (Prolong  \mkleeneopen{}A\mkleeneclose{}  \mkleeneopen{}C'\mkleeneclose{}  `B\mbackslash{}''  \mkleeneopen{}C\mkleeneclose{}  \mkleeneopen{}B\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Assert  \mneg{}(A  =  D')  BY
                          (NotEqualFromEuBetween\mcdot{}  THEN  Auto))
  THEN  (Prolong  \mkleeneopen{}A\mkleeneclose{}  \mkleeneopen{}D'\mkleeneclose{}  `B\mbackslash{}'\mbackslash{}''  \mkleeneopen{}D\mkleeneclose{}  \mkleeneopen{}B\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index