---

Step * of Lemma geo-out-preserves-opp-side-case1

∀e:BasicGeometry. ∀p,q,a,b,c,r,m:Point.
  (p ≠ q ⇒ a-pq-c ⇒ Colinear(p;q;m) ⇒ a=m=c ⇒ Colinear(p;q;r) ⇒ r_b_a ⇒ r ≠ b ⇒ b-pq-c)
BY
{ (Auto THEN (gSeparatedCases ⌜a⌝ ⌜b⌝⋅ THENA Auto)) }

1
1. e : BasicGeometry
2. p : Point
3. q : Point
4. a : Point
5. b : Point
6. c : Point
7. r : Point
8. m : Point
9. p ≠ q
10. a-pq-c
11. Colinear(p;q;m)
12. a=m=c
13. Colinear(p;q;r)
14. r_b_a
15. r ≠ b
16. a ≠ b
⊢ b-pq-c

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}p,q,a,b,c,r,m:Point.
    (p  \mneq{}  q  {}\mRightarrow{}  a-pq-c  {}\mRightarrow{}  Colinear(p;q;m)  {}\mRightarrow{}  a=m=c  {}\mRightarrow{}  Colinear(p;q;r)  {}\mRightarrow{}  r\_b\_a  {}\mRightarrow{}  r  \mneq{}  b  {}\mRightarrow{}  b-pq-c)


By

---

Latex:
(Auto  THEN  (gSeparatedCases  \mkleeneopen{}a\mkleeneclose{}  \mkleeneopen{}b\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index