---

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


1. e : BasicGeometry
2. A : Point
3. B : Point
4. C : Point
5. D : Point
6. B(ABD)
7. B(ABC)
8. A # B
9. ¬B(ACD)
10. ¬B(ADC)
11. A # D
12. A # C
13. D # C
14. C' : Point
15. B(ADC')
16. DC' ≅ CD
17. D' : Point
18. B(ACD')
19. CD' ≅ CD
20. A # C'
21. A # D'
22. C' # C
23. D' # D
24. B' : Point
25. B(AC'B')
26. C'B' ≅ CB
27. B'' : Point
28. B(AD'B'')
29. D'B'' ≅ DB
30. B # C
31. B # D
32. B'' # D'
33. BC' ≅ B''C
⊢ False
BY
{ (Assert B' ≡ B'' BY
         (InstLemma `geo-construction-unicity` [⌜e⌝;⌜A⌝;⌜B⌝;⌜B'⌝;⌜B''⌝]⋅ THEN Auto)) }

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

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

---

Latex:

---

Latex:

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


By

---

Latex:
(Assert  B'  \mequiv{}  B''  BY
              (InstLemma  `geo-construction-unicity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}B'\mkleeneclose{};\mkleeneopen{}B''\mkleeneclose{}]\mcdot{}  THEN  Auto))

---

Home Index