---

Step * of Lemma perp-aux-general-construction

∀e:HeytingGeometry. ∀a,b,c,x:Point.
  (((c # ba ∧ ab  ⊥x cx) ∧ a ≠ x)
  ⇒ (∃c1,c',p:Point. (((c=a=c1 ∧ c=x=c') ∧ c'a ≅ ca) ∧ c' # c1a ∧ ((a # cc' ∧ c1=p=c') ∧ ab  ⊥a pa) ∧ p # ab)))
BY
{ (Auto THEN (D -2 THEN ExRepD) THEN (InstHyp [⌜a⌝;⌜c⌝](9)⋅ THENA Auto) THEN (InstHyp [⌜b⌝;⌜c⌝](9)⋅ THENA Auto)) }

1
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. c # ba
7. Colinear(a;b;x)
8. Colinear(c;x;x)
9. ∀u,v:Point.  (Colinear(a;b;u) ⇒ Colinear(c;x;v) ⇒ Ruxv)
10. a ≠ x
11. Raxc
12. Rbxc
⊢ ∃c1,c',p:Point. (((c=a=c1 ∧ c=x=c') ∧ c'a ≅ ca) ∧ c' # c1a ∧ ((a # cc' ∧ c1=p=c') ∧ ab  ⊥a pa) ∧ p # ab)

---

Latex:

---

Latex:
\mforall{}e:HeytingGeometry.  \mforall{}a,b,c,x:Point.
    (((c  \#  ba  \mwedge{}  ab    \mbot{}x  cx)  \mwedge{}  a  \mneq{}  x)
    {}\mRightarrow{}  (\mexists{}c1,c',p:Point
              (((c=a=c1  \mwedge{}  c=x=c')  \mwedge{}  c'a  \00D0  ca)  \mwedge{}  c'  \#  c1a  \mwedge{}  ((a  \#  cc'  \mwedge{}  c1=p=c')  \mwedge{}  ab    \mbot{}a  pa)  \mwedge{}  p  \#  ab)))


By

---

Latex:
(Auto
  THEN  (D  -2  THEN  ExRepD)
  THEN  (InstHyp  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}](9)\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}](9)\mcdot{}  THENA  Auto))

---

Home Index