---

Step * 2 1 of Lemma geo-perp-unicity


1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. ¬Colinear(a;b;c)
6. u : Point
7. v : Point
8. a ≠ b
9. Colinear(a;b;u)
10. Colinear(a;b;v)
11. ab ⊥ cu
12. ab ⊥ cv
⊢ u ≡ v
BY
{ (((gSeparatedCases ⌜c⌝ ⌜u⌝⋅ THENA Auto) THEN (gSeparatedCases ⌜c⌝ ⌜v⌝⋅ THENA Auto))
   THEN (Assert Rcuv BY
               (D -4
                THEN (InstLemma `geo-perp-in-unicity2` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜u⌝;⌜x⌝;⌜u⌝]⋅ THENA Auto)
                THEN (RWO  "-1<" 0 THENA Auto)
                THEN RepeatFor 2 (D -5)
                THEN (InstHyp [⌜v⌝;⌜c⌝] (-5)⋅ THENA Auto)
                THEN EAuto 1))
   THEN (Assert Rcvu BY
               (D -4
                THEN (InstLemma `geo-perp-in-unicity2` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜v⌝;⌜x⌝;⌜v⌝]⋅ THENA Auto)
                THEN (RWO  "-1<" 0 THENA Auto)
                THEN RepeatFor 2 (D -5)
                THEN (InstHyp [⌜u⌝;⌜c⌝] (-5)⋅ THENA Auto)
                THEN EAuto 1))) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. ¬Colinear(a;b;c)
6. u : Point
7. v : Point
8. a ≠ b
9. Colinear(a;b;u)
10. Colinear(a;b;v)
11. ab ⊥ cu
12. ab ⊥ cv
13. c ≠ u
14. c ≠ v
15. Rcuv
16. Rcvu
⊢ u ≡ v

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  \mneg{}Colinear(a;b;c)
6.  u  :  Point
7.  v  :  Point
8.  a  \mneq{}  b
9.  Colinear(a;b;u)
10.  Colinear(a;b;v)
11.  ab  \mbot{}  cu
12.  ab  \mbot{}  cv
\mvdash{}  u  \mequiv{}  v


By

---

Latex:
(((gSeparatedCases  \mkleeneopen{}c\mkleeneclose{}  \mkleeneopen{}u\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (gSeparatedCases  \mkleeneopen{}c\mkleeneclose{}  \mkleeneopen{}v\mkleeneclose{}\mcdot{}  THENA  Auto))
  THEN  (Assert  Rcuv  BY
                          (D  -4
                            THEN  (InstLemma  `geo-perp-in-unicity2`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  (RWO    "-1<"  0  THENA  Auto)
                            THEN  RepeatFor  2  (D  -5)
                            THEN  (InstHyp  [\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]  (-5)\mcdot{}  THENA  Auto)
                            THEN  EAuto  1))
  THEN  (Assert  Rcvu  BY
                          (D  -4
                            THEN  (InstLemma  `geo-perp-in-unicity2`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  (RWO    "-1<"  0  THENA  Auto)
                            THEN  RepeatFor  2  (D  -5)
                            THEN  (InstHyp  [\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]  (-5)\mcdot{}  THENA  Auto)
                            THEN  EAuto  1)))

---

Home Index