---

Step * 1 1 2 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
34. B' ≡ B''
⊢ False
BY
{ ((Assert B'' ≡ B' BY EAuto 1) THEN (gEliminatePoint (-1) THENA Auto) THEN ThinVar `B\'\'') }

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
⊢ 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
34.  B'  \mequiv{}  B''
\mvdash{}  False


By

---

Latex:
((Assert  B''  \mequiv{}  B'  BY  EAuto  1)  THEN  (gEliminatePoint  (-1)  THENA  Auto)  THEN  ThinVar  `B\mbackslash{}'\mbackslash{}'')

---

Home Index