---

Step * 1 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
⊢ ∃u,v:Point. (Colinear(a;b;u) ∧ Colinear(c;d;v) ∧ u ≠ c ∧ v ≠ c ∧ Rucv)
BY
{ ((InstLemma `geo-sep-or` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝]⋅ THENA Auto) THEN D -1) }

1
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. a ≠ c
⊢ ∃u,v:Point. (Colinear(a;b;u) ∧ Colinear(c;d;v) ∧ u ≠ c ∧ v ≠ c ∧ Rucv)

2
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)

---

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
\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:
((InstLemma  `geo-sep-or`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  D  -1)

---

Home Index