---

Step * of Lemma geo-out-iff-between1

∀e:BasicGeometry. ∀p,a,b,c:Point.  (p ≠ a ⇒ p ≠ b ⇒ p ≠ c ⇒ a_p_c ⇒ (b_p_c ⇐⇒ out(p ab)))
BY
{ (Auto THEN All (Unfolds ``geo-out``) THEN Auto) }

1
1. e : BasicGeometry
2. p : Point
3. a : Point
4. b : Point
5. c : Point
6. p ≠ a
7. p ≠ b
8. p ≠ c
9. a_p_c
10. b_p_c
11. p ≠ a
12. p ≠ b
⊢ ¬((¬p_a_b) ∧ (¬p_b_a))

2
1. e : BasicGeometry
2. p : Point
3. a : Point
4. b : Point
5. c : Point
6. p ≠ a
7. p ≠ b
8. p ≠ c
9. a_p_c
10. p ≠ a
11. p ≠ b
12. ¬((¬p_a_b) ∧ (¬p_b_a))
⊢ b_p_c

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}p,a,b,c:Point.    (p  \mneq{}  a  {}\mRightarrow{}  p  \mneq{}  b  {}\mRightarrow{}  p  \mneq{}  c  {}\mRightarrow{}  a\_p\_c  {}\mRightarrow{}  (b\_p\_c  \mLeftarrow{}{}\mRightarrow{}  out(p  ab)))


By

---

Latex:
(Auto  THEN  All  (Unfolds  ``geo-out``)  THEN  Auto)

---

Home Index