---

Step * of Lemma geo-between-out-implies-out3

No Annotations
∀e:EuclideanPlane. ∀a,b,b',c,c',t:Point.
  (out(a bb') ⇒ out(a cc') ⇒ a-b-c ⇒ B(b'tc') ⇒ a # t ⇒ {(out(a ct) ∧ out(a bt)) ∧ out(a c't) ∧ out(a b't)})
BY
{ (((Auto
     THEN (Assert Colinear(a;c';t) BY
                 ((Assert Colinear(a;b';c') BY
                         Auto)
                  THEN (gSeparatedCases ⌜b'⌝⌜c'⌝⋅ THEN Auto)
                  THEN (Assert t ≡ c' BY
                              (FLemma `geo-between-same` [-4] THEN Auto))
                  THEN EliminatePoint (-1)
                  THEN Auto))
     )
    THEN (Assert Colinear(a;b';t) BY
                ((Assert Colinear(a;b';c') BY Auto) THEN (Assert a # c' BY Auto) THEN Auto))
    )
   THEN skip{RepeatFor 2 ((D 0 THEN Auto))}
   ) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. b' : Point
5. c : Point
6. c' : Point
7. t : Point
8. out(a bb')
9. out(a cc')
10. a-b-c
11. B(b'tc')
12. a # t
13. Colinear(a;c';t)
14. Colinear(a;b';t)
⊢ {(out(a ct) ∧ out(a bt)) ∧ out(a c't) ∧ out(a b't)}

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,b,b',c,c',t:Point.
    (out(a  bb')
    {}\mRightarrow{}  out(a  cc')
    {}\mRightarrow{}  a-b-c
    {}\mRightarrow{}  B(b'tc')
    {}\mRightarrow{}  a  \#  t
    {}\mRightarrow{}  \{(out(a  ct)  \mwedge{}  out(a  bt))  \mwedge{}  out(a  c't)  \mwedge{}  out(a  b't)\})


By

---

Latex:
(((Auto
      THEN  (Assert  Colinear(a;c';t)  BY
                              ((Assert  Colinear(a;b';c')  BY
                                              Auto)
                                THEN  (gSeparatedCases  \mkleeneopen{}b'\mkleeneclose{}\mkleeneopen{}c'\mkleeneclose{}\mcdot{}  THEN  Auto)
                                THEN  (Assert  t  \mequiv{}  c'  BY
                                                        (FLemma  `geo-between-same`  [-4]  THEN  Auto))
                                THEN  EliminatePoint  (-1)
                                THEN  Auto))
      )
    THEN  (Assert  Colinear(a;b';t)  BY
                            ((Assert  Colinear(a;b';c')  BY  Auto)  THEN  (Assert  a  \#  c'  BY  Auto)  THEN  Auto))
    )
  THEN  skip\{RepeatFor  2  ((D  0  THEN  Auto))\}
  )

---

Home Index