---

Step * 1 1 2 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
⊢ False
BY
{ (InstLemma `geo-five-segment` [⌜e⌝;⌜B⌝; ⌜C⌝;⌜D'⌝;⌜C'⌝;⌜B'⌝;⌜C'⌝;⌜D⌝;⌜C⌝]⋅ THENA Auto) }

1
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

---

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
\mvdash{}  False


By

---

Latex:
(InstLemma  `geo-five-segment`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};  \mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}D'\mkleeneclose{};\mkleeneopen{}C'\mkleeneclose{};\mkleeneopen{}B'\mkleeneclose{};\mkleeneopen{}C'\mkleeneclose{};\mkleeneopen{}D\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index