---

Step * of Lemma perp-aux1

∀e:HeytingGeometry. ∀a,b,c,p,q,r:Point.  (a # bc ⇒ a-p-b ⇒ c-q-b ⇒ a-r-c ⇒ (∃y:Point. (p-y-c ∧ q-y-r)))
BY
{ (Auto THEN (InstLemma `geo-inner-pasch-ex` [⌜e⌝;⌜a⌝;⌜c⌝;⌜b⌝;⌜p⌝;⌜q⌝]⋅ THENA Auto)) }

1
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. p : Point
6. q : Point
7. r : Point
8. a # bc
9. a-p-b
10. c-q-b
11. a-r-c
12. ∃x:Point. (c-x-p ∧ a-x-q)
⊢ ∃y:Point. (p-y-c ∧ q-y-r)

---

Latex:

---

Latex:
\mforall{}e:HeytingGeometry.  \mforall{}a,b,c,p,q,r:Point.
    (a  \#  bc  {}\mRightarrow{}  a-p-b  {}\mRightarrow{}  c-q-b  {}\mRightarrow{}  a-r-c  {}\mRightarrow{}  (\mexists{}y:Point.  (p-y-c  \mwedge{}  q-y-r)))


By

---

Latex:
(Auto  THEN  (InstLemma  `geo-inner-pasch-ex`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index