---

Step * 1 2 of Lemma geo-perp-in-iff2


1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a ≠ b
7. c ≠ d
8. ab  ⊥c cd
⇒ (Colinear(a;b;c) ∧ Colinear(c;d;c) ∧ (∃u,v:Point. (Colinear(a;b;u) ∧ Colinear(c;d;v) ∧ u ≠ c ∧ v ≠ c ∧ Rucv)))
9. ab  ⊥c cd ⇐ Colinear(a;b;c)
∧ Colinear(c;d;c)
∧ (∃u,v:Point. (Colinear(a;b;u) ∧ Colinear(c;d;v) ∧ u ≠ c ∧ v ≠ c ∧ Rucv))
10. Colinear(a;b;c)
11. Racd
12. Rbcd
13. b ≠ c
⊢ ∃u,v:Point. (Colinear(a;b;u) ∧ Colinear(c;d;v) ∧ u ≠ c ∧ v ≠ c ∧ Rucv)
BY
{ (InstConcl [⌜b⌝;⌜d⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  a  \mneq{}  b
7.  c  \mneq{}  d
8.  ab    \mbot{}c  cd
{}\mRightarrow{}  (Colinear(a;b;c)
      \mwedge{}  Colinear(c;d;c)
      \mwedge{}  (\mexists{}u,v:Point.  (Colinear(a;b;u)  \mwedge{}  Colinear(c;d;v)  \mwedge{}  u  \mneq{}  c  \mwedge{}  v  \mneq{}  c  \mwedge{}  Rucv)))
9.  ab    \mbot{}c  cd  \mLeftarrow{}{}  Colinear(a;b;c)
\mwedge{}  Colinear(c;d;c)
\mwedge{}  (\mexists{}u,v:Point.  (Colinear(a;b;u)  \mwedge{}  Colinear(c;d;v)  \mwedge{}  u  \mneq{}  c  \mwedge{}  v  \mneq{}  c  \mwedge{}  Rucv))
10.  Colinear(a;b;c)
11.  Racd
12.  Rbcd
13.  b  \mneq{}  c
\mvdash{}  \mexists{}u,v:Point.  (Colinear(a;b;u)  \mwedge{}  Colinear(c;d;v)  \mwedge{}  u  \mneq{}  c  \mwedge{}  v  \mneq{}  c  \mwedge{}  Rucv)


By

---

Latex:
(InstConcl  [\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index