---

Step * of Lemma geo-between-same-side

No Annotations
∀e:BasicGeometry. ∀[A,B,C,D:Point].  (¬((¬B(ACD)) ∧ (¬B(ADC)))) supposing (A # B and B(ABC) and B(ABD))
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN (gProveSeparatedWhenStable ⌜A⌝ ⌜D⌝⋅ THENA Auto)
   THEN (gProveSeparatedWhenStable ⌜A⌝ ⌜C⌝⋅ THENA Auto)
   THEN (gProveSeparatedWhenStable ⌜D⌝ ⌜C⌝⋅ THENA Auto)
   THEN (gProlong ⌜A⌝ ⌜D⌝ `C\'' ⌜C⌝ ⌜D⌝⋅ THENA Auto)
   THEN (gProlong ⌜A⌝ ⌜C⌝ `D\'' ⌜C⌝ ⌜D⌝⋅ THENA Auto)
   THEN ExRepD
   THEN ((gProveSeparatedWhenStable ⌜A⌝ ⌜C'⌝⋅ THENA Auto)
         THEN (gProveSeparatedWhenStable ⌜A⌝ ⌜D'⌝⋅ THENA Auto)
         THEN (gProveSeparatedWhenStable ⌜C'⌝ ⌜C⌝⋅ THENA Auto)
         THEN (gProveSeparatedWhenStable ⌜D'⌝ ⌜D⌝⋅ THENA Auto))
   THEN (gProlong ⌜A⌝ ⌜C'⌝ `B\'' ⌜C⌝ ⌜B⌝⋅ THENA Auto)
   THEN (gProlong ⌜A⌝ ⌜D'⌝ `B\'\'' ⌜D⌝ ⌜B⌝⋅ THENA Auto)) }

1
1. e : BasicGeometry
2. A : Point
3. B : Point
4. C : Point
5. D : Point
6. B(ABD)
7. B(ABC)
8. A # B
9. ¬B(ACD)
10. ¬B(ADC)
11. A # D
12. A # C
13. D # C
14. C' : Point
15. B(ADC')
16. DC' ≅ CD
17. D' : Point
18. B(ACD')
19. CD' ≅ CD
20. A # C'
21. A # D'
22. C' # C
23. D' # D
24. B' : Point
25. B(AC'B') ∧ C'B' ≅ CB
26. B'' : Point
27. B(AD'B'') ∧ D'B'' ≅ DB
⊢ False

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:BasicGeometry
    \mforall{}[A,B,C,D:Point].    (\mneg{}((\mneg{}B(ACD))  \mwedge{}  (\mneg{}B(ADC))))  supposing  (A  \#  B  and  B(ABC)  and  B(ABD))


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  (gProveSeparatedWhenStable  \mkleeneopen{}A\mkleeneclose{}  \mkleeneopen{}D\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (gProveSeparatedWhenStable  \mkleeneopen{}A\mkleeneclose{}  \mkleeneopen{}C\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (gProveSeparatedWhenStable  \mkleeneopen{}D\mkleeneclose{}  \mkleeneopen{}C\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (gProlong  \mkleeneopen{}A\mkleeneclose{}  \mkleeneopen{}D\mkleeneclose{}  `C\mbackslash{}''  \mkleeneopen{}C\mkleeneclose{}  \mkleeneopen{}D\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (gProlong  \mkleeneopen{}A\mkleeneclose{}  \mkleeneopen{}C\mkleeneclose{}  `D\mbackslash{}''  \mkleeneopen{}C\mkleeneclose{}  \mkleeneopen{}D\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  ((gProveSeparatedWhenStable  \mkleeneopen{}A\mkleeneclose{}  \mkleeneopen{}C'\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  (gProveSeparatedWhenStable  \mkleeneopen{}A\mkleeneclose{}  \mkleeneopen{}D'\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  (gProveSeparatedWhenStable  \mkleeneopen{}C'\mkleeneclose{}  \mkleeneopen{}C\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  (gProveSeparatedWhenStable  \mkleeneopen{}D'\mkleeneclose{}  \mkleeneopen{}D\mkleeneclose{}\mcdot{}  THENA  Auto))
  THEN  (gProlong  \mkleeneopen{}A\mkleeneclose{}  \mkleeneopen{}C'\mkleeneclose{}  `B\mbackslash{}''  \mkleeneopen{}C\mkleeneclose{}  \mkleeneopen{}B\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (gProlong  \mkleeneopen{}A\mkleeneclose{}  \mkleeneopen{}D'\mkleeneclose{}  `B\mbackslash{}'\mbackslash{}''  \mkleeneopen{}D\mkleeneclose{}  \mkleeneopen{}B\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index