---

Step * of Lemma rv-be-five-segment

∀a,b,c,d,A,B,C,D:ℝ^2.  (a ≠ b ⇒ a_b_c ⇒ A_B_C ⇒ ab=AB ⇒ bc=BC ⇒ ad=AD ⇒ bd=BD ⇒ cd=CD)
BY
{ ((InstLemma `rv-five-segment` [⌜2⌝]⋅ THENA Auto) THEN RepeatFor 8 (ParallelLast') THEN 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
⊢ cd=CD

---

Latex:

---

Latex:
\mforall{}a,b,c,d,A,B,C,D:\mBbbR{}\^{}2.    (a  \mneq{}  b  {}\mRightarrow{}  a\_b\_c  {}\mRightarrow{}  A\_B\_C  {}\mRightarrow{}  ab=AB  {}\mRightarrow{}  bc=BC  {}\mRightarrow{}  ad=AD  {}\mRightarrow{}  bd=BD  {}\mRightarrow{}  cd=CD)


By

---

Latex:
((InstLemma  `rv-five-segment`  [\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  RepeatFor  8  (ParallelLast')  THEN  Auto)

---

Home Index