---

Step * of Lemma geo-bet-out-out-bet

∀e:BasicGeometry. ∀b,a,a',c,c':Point.  (a_b_c ⇒ out(b aa') ⇒ out(b cc') ⇒ a'_b_c')
BY
{ (Unfold `geo-out` 0 THEN Auto THEN GeoContradiction) }

1
1. e : BasicGeometry
2. b : Point
3. a : Point
4. a' : Point
5. c : Point
6. c' : Point
7. a_b_c
8. b ≠ a
9. b ≠ a'
10. ¬((¬b_a_a') ∧ (¬b_a'_a))
11. b ≠ c
12. b ≠ c'
13. ¬((¬b_c_c') ∧ (¬b_c'_c))
14. ¬a'_b_c'
⊢ False

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}b,a,a',c,c':Point.    (a\_b\_c  {}\mRightarrow{}  out(b  aa')  {}\mRightarrow{}  out(b  cc')  {}\mRightarrow{}  a'\_b\_c')


By

---

Latex:
(Unfold  `geo-out`  0  THEN  Auto  THEN  GeoContradiction)

---

Home Index