---

Step * 1 of Lemma rv-be-five-segment


1. a : ℝ^2
2. b : ℝ^2
3. c : ℝ^2
4. d : ℝ^2
5. A : ℝ^2
6. B : ℝ^2
7. C : ℝ^2
8. D : ℝ^2
9. (cd=CD) supposing (bd=BD and ad=AD and bc=BC and ab=AB and A-B-C and a-b-c)
10. a ≠ b
11. a_b_c
12. A_B_C
13. ab=AB
14. bc=BC
15. ad=AD
16. bd=BD
⊢ cd=CD
BY
{ (StableCases ⌜a-b-c⌝⋅ THENA Auto) }

1
1. a : ℝ^2
2. b : ℝ^2
3. c : ℝ^2
4. d : ℝ^2
5. A : ℝ^2
6. B : ℝ^2
7. C : ℝ^2
8. D : ℝ^2
9. (cd=CD) supposing (bd=BD and ad=AD and bc=BC and ab=AB and A-B-C and a-b-c)
10. a ≠ b
11. a_b_c
12. A_B_C
13. ab=AB
14. bc=BC
15. ad=AD
16. bd=BD
17. a-b-c
⊢ cd=CD

2
1. a : ℝ^2
2. b : ℝ^2
3. c : ℝ^2
4. d : ℝ^2
5. A : ℝ^2
6. B : ℝ^2
7. C : ℝ^2
8. D : ℝ^2
9. (cd=CD) supposing (bd=BD and ad=AD and bc=BC and ab=AB and A-B-C and a-b-c)
10. a ≠ b
11. a_b_c
12. A_B_C
13. ab=AB
14. bc=BC
15. ad=AD
16. bd=BD
17. ¬a-b-c
⊢ cd=CD

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}\^{}2
2.  b  :  \mBbbR{}\^{}2
3.  c  :  \mBbbR{}\^{}2
4.  d  :  \mBbbR{}\^{}2
5.  A  :  \mBbbR{}\^{}2
6.  B  :  \mBbbR{}\^{}2
7.  C  :  \mBbbR{}\^{}2
8.  D  :  \mBbbR{}\^{}2
9.  (cd=CD)  supposing  (bd=BD  and  ad=AD  and  bc=BC  and  ab=AB  and  A-B-C  and  a-b-c)
10.  a  \mneq{}  b
11.  a\_b\_c
12.  A\_B\_C
13.  ab=AB
14.  bc=BC
15.  ad=AD
16.  bd=BD
\mvdash{}  cd=CD


By

---

Latex:
(StableCases  \mkleeneopen{}a-b-c\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index