---

Step * of Lemma geo-out2-bet

∀e:BasicGeometry. ∀a,b,c:Point.  (out(a bc) ⇒ out(c ab) ⇒ a_b_c)
BY
{ (Auto
   THEN D -2
   THEN D -1
   THEN ExRepD
   THEN ((DoubleNegation THENM D 0) THENA Auto)
   THEN ∀h:hyp. (DNot h THEN DAnd 0 THEN (DNot 0 THENA Auto)) ) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a ≠ b
6. a ≠ c
7. c ≠ a
8. c ≠ b
9. ¬a_b_c
10. c_a_b
11. a_b_c
⊢ False

2
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a ≠ b
6. a ≠ c
7. c ≠ a
8. c ≠ b
9. ¬a_b_c
10. c_a_b
11. a_c_b
⊢ False

3
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a ≠ b
6. a ≠ c
7. c ≠ a
8. c ≠ b
9. ¬a_b_c
10. c_b_a
11. a_b_c
⊢ False

4
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a ≠ b
6. a ≠ c
7. c ≠ a
8. c ≠ b
9. ¬a_b_c
10. c_b_a
11. a_c_b
⊢ False

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  D  -2
  THEN  D  -1
  THEN  ExRepD
  THEN  ((DoubleNegation  THENM  D  0)  THENA  Auto)
  THEN  \mforall{}h:hyp.  (DNot  h  THEN  DAnd  0  THEN  (DNot  0  THENA  Auto))  )

---

Home Index