---

Step * of Lemma ip-inner-Pasch'

∀rv:InnerProductSpace. ∀a,b:Point. ∀c:{c:Point| b # c} . ∀p:{p:Point| a_p_c ∧ a # p} . ∀q:{q:Point| b_q_c} .
  (∃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-Pasch` []
   THEN RepeatFor 6 ((ParallelLast' THENA Auto))
   THEN RepeatFor 2 ((D -1 THENA Auto))
   THEN ExRepD
   THEN D 0 With ⌜x⌝ 
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}rv:InnerProductSpace.  \mforall{}a,b:Point.  \mforall{}c:\{c:Point|  b  \#  c\}  .  \mforall{}p:\{p:Point|  a\_p\_c  \mwedge{}  a  \#  p\}  .  \mforall{}q:\{q:Point| 
                                                                                                                                                                                  b\_q\_c\}  .
    (\mexists{}x:\{Point|  (a\_x\_q
                            \mwedge{}  b\_x\_p
                            \mwedge{}  (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-Pasch`  []
  THEN  RepeatFor  6  ((ParallelLast'  THENA  Auto))
  THEN  RepeatFor  2  ((D  -1  THENA  Auto))
  THEN  ExRepD
  THEN  D  0  With  \mkleeneopen{}x\mkleeneclose{} 
  THEN  Auto)

---

Home Index