---

Step * of Lemma geo-perp-in-iff2

∀e:BasicGeometry. ∀a,b,c,d:Point.  (a ≠ b ⇒ c ≠ d ⇒ (ab  ⊥c cd ⇐⇒ Colinear(a;b;c) ∧ Racd ∧ Rbcd))
BY
{ (InstLemma `geo-perp-in-iff` []
   THEN RepeatFor 5 ((ParallelLast' THENA Auto))
   THEN (D -1 With ⌜c⌝  THENA Auto)
   THEN RepeatFor 2 ((ParallelLast' THENA Auto))
   THEN RWO "-1" 0
   THEN Auto) }

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

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,d:Point.    (a  \mneq{}  b  {}\mRightarrow{}  c  \mneq{}  d  {}\mRightarrow{}  (ab    \mbot{}c  cd  \mLeftarrow{}{}\mRightarrow{}  Colinear(a;b;c)  \mwedge{}  Racd  \mwedge{}  Rbcd))


By

---

Latex:
(InstLemma  `geo-perp-in-iff`  []
  THEN  RepeatFor  5  ((ParallelLast'  THENA  Auto))
  THEN  (D  -1  With  \mkleeneopen{}c\mkleeneclose{}    THENA  Auto)
  THEN  RepeatFor  2  ((ParallelLast'  THENA  Auto))
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index