---

Step * 1 of Lemma geo-colinear-left-out3


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. c' : Point
7. x : Point
8. x' : Point
9. Colinear(b;x;x')
10. a-x-c
11. a'-x'-c'
12. out(b aa')
13. out(b cc')
14. b leftof ac
15. b leftof a'c'
16. b leftof ax
17. b leftof a'x'
18. b # x'
19. ¬B(bxx')
20. ¬B(bx'x)
21. x'-b-x
⊢ False
BY
{ ((FLemma `left-all-symmetry` [16] THENA Auto) THEN (FLemma `left-all-symmetry` [17] THENA Auto)) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. c' : Point
7. x : Point
8. x' : Point
9. Colinear(b;x;x')
10. a-x-c
11. a'-x'-c'
12. out(b aa')
13. out(b cc')
14. b leftof ac
15. b leftof a'c'
16. b leftof ax
17. b leftof a'x'
18. b # x'
19. ¬B(bxx')
20. ¬B(bx'x)
21. x'-b-x
22. a leftof xb ∧ x leftof ba
23. a' leftof x'b ∧ x' leftof ba'
⊢ False

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  a'  :  Point
6.  c'  :  Point
7.  x  :  Point
8.  x'  :  Point
9.  Colinear(b;x;x')
10.  a-x-c
11.  a'-x'-c'
12.  out(b  aa')
13.  out(b  cc')
14.  b  leftof  ac
15.  b  leftof  a'c'
16.  b  leftof  ax
17.  b  leftof  a'x'
18.  b  \#  x'
19.  \mneg{}B(bxx')
20.  \mneg{}B(bx'x)
21.  x'-b-x
\mvdash{}  False


By

---

Latex:
((FLemma  `left-all-symmetry`  [16]  THENA  Auto)  THEN  (FLemma  `left-all-symmetry`  [17]  THENA  Auto))

---

Home Index