---

Step * 1 of Lemma geo-perp-in-symmetry


1. e : BasicGeometry
2. x : Point
3. [a] : Point
4. [b] : Point
5. [c] : Point
6. [d] : Point
7. ab  ⊥x cd
8. ∀x:Point. ∀[a,b,c,d:Point].  (ab  ⊥x cd ⇒ cd  ⊥x ab)
9. ∀x:Point. ∀[a,b,c,d:Point].  (ab  ⊥x cd ⇒ ba  ⊥x cd)
⊢ ab  ⊥x dc
BY
{ (BHyp -2  THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  x  :  Point
3.  [a]  :  Point
4.  [b]  :  Point
5.  [c]  :  Point
6.  [d]  :  Point
7.  ab    \mbot{}x  cd
8.  \mforall{}x:Point.  \mforall{}[a,b,c,d:Point].    (ab    \mbot{}x  cd  {}\mRightarrow{}  cd    \mbot{}x  ab)
9.  \mforall{}x:Point.  \mforall{}[a,b,c,d:Point].    (ab    \mbot{}x  cd  {}\mRightarrow{}  ba    \mbot{}x  cd)
\mvdash{}  ab    \mbot{}x  dc


By

---

Latex:
(BHyp  -2    THEN  Auto)

---

Home Index