---

Step * of Lemma geo-perp-in-iff

∀e:BasicGeometry. ∀a,b,c,d,x:Point.
  (a ≠ b
  ⇒ c ≠ d
  ⇒ (ab  ⊥x cd
     ⇐⇒ Colinear(a;b;x) ∧ Colinear(c;d;x) ∧ (∃u,v:Point. (Colinear(a;b;u) ∧ Colinear(c;d;v) ∧ u ≠ x ∧ v ≠ x ∧ Ruxv))))
BY
{ Auto }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. x : Point
7. a ≠ b
8. c ≠ d
9. ab  ⊥x cd
⊢ ∃u,v:Point. (Colinear(a;b;u) ∧ Colinear(c;d;v) ∧ u ≠ x ∧ v ≠ x ∧ Ruxv)

2
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. x : Point
7. a ≠ b
8. c ≠ d
9. Colinear(a;b;x)
10. Colinear(c;d;x)
11. ∃u,v:Point. (Colinear(a;b;u) ∧ Colinear(c;d;v) ∧ u ≠ x ∧ v ≠ x ∧ Ruxv)
⊢ ab  ⊥x cd

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,d,x:Point.
    (a  \mneq{}  b
    {}\mRightarrow{}  c  \mneq{}  d
    {}\mRightarrow{}  (ab    \mbot{}x  cd
          \mLeftarrow{}{}\mRightarrow{}  Colinear(a;b;x)
                  \mwedge{}  Colinear(c;d;x)
                  \mwedge{}  (\mexists{}u,v:Point.  (Colinear(a;b;u)  \mwedge{}  Colinear(c;d;v)  \mwedge{}  u  \mneq{}  x  \mwedge{}  v  \mneq{}  x  \mwedge{}  Ruxv))))


By

---

Latex:
Auto

---

Home Index