---

Step * of Lemma ip-five-segment

∀[rv:InnerProductSpace]. ∀[a,b,c,d,A,B,C,D:Point].
  (cd=CD) supposing (bd=BD and ad=AD and bc=BC and ab=AB and A_B_C and a_b_c and a # b)
BY
{ (Auto
   THEN ((FLemma `ip-dist-between` [-6] THENA Auto) THEN PromoteHyp (-1) 10)
   THEN (FLemma `ip-dist-between` [-5] THENA Auto)
   THEN PromoteHyp (-1) 10) }

1
1. rv : InnerProductSpace
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. A : Point
7. B : Point
8. C : Point
9. D : Point
10. ||A - C|| = (||A - B|| + ||B - C||)
11. ||a - c|| = (||a - b|| + ||b - c||)
12. a # b
13. a_b_c
14. A_B_C
15. ab=AB
16. bc=BC
17. ad=AD
18. bd=BD
⊢ cd=CD

---

Latex:

---

Latex:
\mforall{}[rv:InnerProductSpace].  \mforall{}[a,b,c,d,A,B,C,D:Point].
    (cd=CD)  supposing  (bd=BD  and  ad=AD  and  bc=BC  and  ab=AB  and  A\_B\_C  and  a\_b\_c  and  a  \#  b)


By

---

Latex:
(Auto
  THEN  ((FLemma  `ip-dist-between`  [-6]  THENA  Auto)  THEN  PromoteHyp  (-1)  10)
  THEN  (FLemma  `ip-dist-between`  [-5]  THENA  Auto)
  THEN  PromoteHyp  (-1)  10)

---

Home Index