---

Step * 1 2 2 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
17. ¬a-b-c
18. ¬b ≠ c
⊢ cd=CD
BY
{ (RWO  "not-real-vec-sep-iff-eq" (-1) 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
18. req-vec(2;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
17.  \mneg{}a-b-c
18.  \mneg{}b  \mneq{}  c
\mvdash{}  cd=CD


By

---

Latex:
(RWO    "not-real-vec-sep-iff-eq"  (-1)  THENA  Auto)

---

Home Index