---

Step * 1 1 2 1 1 of Lemma geo-between-same-side


1. e : BasicGeometry
2. B' : Point
3. A : Point
4. B : Point
5. C : Point
6. D : Point
7. B(ABD)
8. B(ABC)
9. A # B
10. ¬B(ACD)
11. ¬B(ADC)
12. A # D
13. A # C
14. D # C
15. C' : Point
16. B(ADC')
17. DC' ≅ CD
18. D' : Point
19. B(ACD')
20. CD' ≅ CD
21. A # C'
22. A # D'
23. C' # C
24. D' # D
25. B(AC'B')
26. C'B' ≅ CB
27. B(AD'B')
28. D'B' ≅ DB
29. B # C
30. B # D
31. B' # D'
32. BC' ≅ B'C
33. D'C' ≅ DC
⊢ False
BY
{ (Assert ⌜¬¬(∃E:Point. (B(CEC') ∧ B(DED')))⌝⋅ THENM (D -1 THEN (D 0 THENA Auto) THEN ExRepD)) }

1
.....assertion..... 
1. e : BasicGeometry
2. B' : Point
3. A : Point
4. B : Point
5. C : Point
6. D : Point
7. B(ABD)
8. B(ABC)
9. A # B
10. ¬B(ACD)
11. ¬B(ADC)
12. A # D
13. A # C
14. D # C
15. C' : Point
16. B(ADC')
17. DC' ≅ CD
18. D' : Point
19. B(ACD')
20. CD' ≅ CD
21. A # C'
22. A # D'
23. C' # C
24. D' # D
25. B(AC'B')
26. C'B' ≅ CB
27. B(AD'B')
28. D'B' ≅ DB
29. B # C
30. B # D
31. B' # D'
32. BC' ≅ B'C
33. D'C' ≅ DC
⊢ ¬¬(∃E:Point. (B(CEC') ∧ B(DED')))

2
1. e : BasicGeometry
2. B' : Point
3. A : Point
4. B : Point
5. C : Point
6. D : Point
7. B(ABD)
8. B(ABC)
9. A # B
10. ¬B(ACD)
11. ¬B(ADC)
12. A # D
13. A # C
14. D # C
15. C' : Point
16. B(ADC')
17. DC' ≅ CD
18. D' : Point
19. B(ACD')
20. CD' ≅ CD
21. A # C'
22. A # D'
23. C' # C
24. D' # D
25. B(AC'B')
26. C'B' ≅ CB
27. B(AD'B')
28. D'B' ≅ DB
29. B # C
30. B # D
31. B' # D'
32. BC' ≅ B'C
33. D'C' ≅ DC
34. E : Point
35. B(CEC')
36. B(DED')
⊢ False

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  B'  :  Point
3.  A  :  Point
4.  B  :  Point
5.  C  :  Point
6.  D  :  Point
7.  B(ABD)
8.  B(ABC)
9.  A  \#  B
10.  \mneg{}B(ACD)
11.  \mneg{}B(ADC)
12.  A  \#  D
13.  A  \#  C
14.  D  \#  C
15.  C'  :  Point
16.  B(ADC')
17.  DC'  \mcong{}  CD
18.  D'  :  Point
19.  B(ACD')
20.  CD'  \mcong{}  CD
21.  A  \#  C'
22.  A  \#  D'
23.  C'  \#  C
24.  D'  \#  D
25.  B(AC'B')
26.  C'B'  \mcong{}  CB
27.  B(AD'B')
28.  D'B'  \mcong{}  DB
29.  B  \#  C
30.  B  \#  D
31.  B'  \#  D'
32.  BC'  \mcong{}  B'C
33.  D'C'  \mcong{}  DC
\mvdash{}  False


By

---

Latex:
(Assert  \mkleeneopen{}\mneg{}\mneg{}(\mexists{}E:Point.  (B(CEC')  \mwedge{}  B(DED')))\mkleeneclose{}\mcdot{}  THENM  (D  -1  THEN  (D  0  THENA  Auto)  THEN  ExRepD))

---

Home Index