---

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

∀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) ⇒ out(r ab) ⇒ b-pq-c)
BY
{ (Auto THEN (gSeparatedCases ⌜a⌝ ⌜b⌝⋅ THENA Auto) THEN (StableCases ⌜r_b_a⌝⋅ 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. out(r ab)
15. a ≠ b
16. r_b_a
⊢ b-pq-c

2
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. out(r ab)
15. a ≠ b
16. ¬r_b_a
⊢ 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{}  out(r  ab)  {}\mRightarrow{}  b-pq-c)


By

---

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

---

Home Index