---

Step * of Lemma ip-inner-Pasch

∀rv:InnerProductSpace. ∀a,b,c:Point. ∀p:{p:Point| a_p_c} . ∀q:{q:Point| b_q_c} .
  (a # p
  ⇒ b # c
  ⇒ (∃x:{x:Point| a_x_q ∧ b_x_p} 
       ((a # q ⇒ x # a)
       ∧ ((a # q ∧ p # c ∧ b # q) ⇒ x # q)
       ∧ ((b # p ∧ b # q) ⇒ x # b)
       ∧ ((b # p ∧ q # c) ⇒ x # p))))
BY
{ (InstLemma  `ip-inner-Pasch1` []
   THEN RepeatFor 8 ((ParallelLast' THENA Auto))
   THEN RepeatFor 2 ((D -1 THENA Auto))
   THEN ParallelLast
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}a,b,c:Point.  \mforall{}p:\{p:Point|  a\_p\_c\}  .  \mforall{}q:\{q:Point|  b\_q\_c\}  .
    (a  \#  p
    {}\mRightarrow{}  b  \#  c
    {}\mRightarrow{}  (\mexists{}x:\{x:Point|  a\_x\_q  \mwedge{}  b\_x\_p\} 
              ((a  \#  q  {}\mRightarrow{}  x  \#  a)
              \mwedge{}  ((a  \#  q  \mwedge{}  p  \#  c  \mwedge{}  b  \#  q)  {}\mRightarrow{}  x  \#  q)
              \mwedge{}  ((b  \#  p  \mwedge{}  b  \#  q)  {}\mRightarrow{}  x  \#  b)
              \mwedge{}  ((b  \#  p  \mwedge{}  q  \#  c)  {}\mRightarrow{}  x  \#  p))))


By

---

Latex:
(InstLemma    `ip-inner-Pasch1`  []
  THEN  RepeatFor  8  ((ParallelLast'  THENA  Auto))
  THEN  RepeatFor  2  ((D  -1  THENA  Auto))
  THEN  ParallelLast
  THEN  Auto)

---

Home Index