---

Step * of Lemma perp-aux-separations

∀e:HeytingGeometry. ∀a,b,c,x,c1,c',p:Point.
  ((((c # ba ∧ ab  ⊥x cx) ∧ a ≠ x)
  ∧ ((c=a=c1 ∧ c=x=c') ∧ c'a ≅ ca)
  ∧ c' # c1a
  ∧ ((a # cc' ∧ c1=p=c') ∧ ab  ⊥a pa)
  ∧ p # ab)
  ⇒ ((c' ≠ c1 ∧ c ≠ x ∧ (c' ≠ x ∧ c1 ≠ p) ∧ c' ≠ p ∧ c ≠ c1) ∧ c # c'c1))
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}e:HeytingGeometry.  \mforall{}a,b,c,x,c1,c',p:Point.
    ((((c  \#  ba  \mwedge{}  ab    \mbot{}x  cx)  \mwedge{}  a  \mneq{}  x)
    \mwedge{}  ((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)
    {}\mRightarrow{}  ((c'  \mneq{}  c1  \mwedge{}  c  \mneq{}  x  \mwedge{}  (c'  \mneq{}  x  \mwedge{}  c1  \mneq{}  p)  \mwedge{}  c'  \mneq{}  p  \mwedge{}  c  \mneq{}  c1)  \mwedge{}  c  \#  c'c1))


By

---

Latex:
Auto

---

Home Index