---

Step * of Lemma geo-out2-bet-out

∀e:BasicGeometry. ∀a,b,c,x,p:Point.  (out(b ac) ⇒ out(b xp) ⇒ a_x_c ⇒ {out(b ap) ∧ out(b cp)})
BY
{ (Auto
   THEN D -3
   THEN D -2
   THEN ExRepD
   THEN RepeatFor 4 (((D 0 THENA Auto) THEN Try (Trivial)))
   THEN ExRepD
   THEN ∀h:hyp. (DNot h THEN DAnd 0 THEN (D 0 THENA Auto)) ) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. p : Point
7. b ≠ a
8. b ≠ c
9. b ≠ x
10. b ≠ p
11. a_x_c
12. ¬b_a_p
13. ¬b_p_a
14. b_x_p
15. b_a_c
⊢ False

2
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. p : Point
7. b ≠ a
8. b ≠ c
9. b ≠ x
10. b ≠ p
11. a_x_c
12. ¬b_a_p
13. ¬b_p_a
14. b_x_p
15. b_c_a
⊢ False

3
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. p : Point
7. b ≠ a
8. b ≠ c
9. b ≠ x
10. b ≠ p
11. a_x_c
12. ¬b_a_p
13. ¬b_p_a
14. b_p_x
15. b_a_c
⊢ False

4
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. p : Point
7. b ≠ a
8. b ≠ c
9. b ≠ x
10. b ≠ p
11. a_x_c
12. ¬b_a_p
13. ¬b_p_a
14. b_p_x
15. b_c_a
⊢ False

5
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. p : Point
7. b ≠ a
8. b ≠ c
9. b ≠ x
10. b ≠ p
11. a_x_c
12. ¬b_c_p
13. ¬b_p_c
14. b_x_p
15. b_a_c
⊢ False

6
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. p : Point
7. b ≠ a
8. b ≠ c
9. b ≠ x
10. b ≠ p
11. a_x_c
12. ¬b_c_p
13. ¬b_p_c
14. b_x_p
15. b_c_a
⊢ False

7
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. p : Point
7. b ≠ a
8. b ≠ c
9. b ≠ x
10. b ≠ p
11. a_x_c
12. ¬b_c_p
13. ¬b_p_c
14. b_p_x
15. b_a_c
⊢ False

8
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. p : Point
7. b ≠ a
8. b ≠ c
9. b ≠ x
10. b ≠ p
11. a_x_c
12. ¬b_c_p
13. ¬b_p_c
14. b_p_x
15. b_c_a
⊢ False

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,x,p:Point.    (out(b  ac)  {}\mRightarrow{}  out(b  xp)  {}\mRightarrow{}  a\_x\_c  {}\mRightarrow{}  \{out(b  ap)  \mwedge{}  out(b  cp)\})


By

---

Latex:
(Auto
  THEN  D  -3
  THEN  D  -2
  THEN  ExRepD
  THEN  RepeatFor  4  (((D  0  THENA  Auto)  THEN  Try  (Trivial)))
  THEN  ExRepD
  THEN  \mforall{}h:hyp.  (DNot  h  THEN  DAnd  0  THEN  (D  0  THENA  Auto))  )

---

Home Index