---

Step * of Lemma ip-extend

∀rv:InnerProductSpace. ∀a:Point. ∀b:{b:Point| a # b} . ∀c,d:Point.  (∃x:{Point| (a_b_x ∧ bx=cd)})
BY
{ (((InstLemma `ip-extend-lemma` [] THEN RepeatFor 3 (ParallelLast')) THEN Auto)
   THEN (InstHyp [⌜||c - d||⌝] (-3)⋅ THENA Auto)
   THEN ParallelLast
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}a:Point.  \mforall{}b:\{b:Point|  a  \#  b\}  .  \mforall{}c,d:Point.    (\mexists{}x:\{Point|  (a\_b\_x  \mwedge{}  bx=cd)\})


By

---

Latex:
(((InstLemma  `ip-extend-lemma`  []  THEN  RepeatFor  3  (ParallelLast'))  THEN  Auto)
  THEN  (InstHyp  [\mkleeneopen{}||c  -  d||\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
  THEN  ParallelLast
  THEN  Auto)

---

Home Index