---

Step * of Lemma geo-lt-implies-gt-strong-1

No Annotations
∀g:EuclideanPlane. ∀a,b,c,d:Point.  (|cd| < |ab| ⇒ (∃w:Point. (B(awb) ∧ aw ≅ cd ∧ w # b)))
BY
{ (Auto
   THEN (Assert a # b BY
               (FLemma `geo-lt-sep` [-1] THEN Auto))
   THEN ((gProperProlong  ⌜b⌝⌜a⌝`A'⌜b⌝⌜a⌝⋅ THENA Auto) THEN ExRepD)
   THEN ((gProlong  ⌜A⌝⌜a⌝`w'⌜c⌝⌜d⌝⋅ THENA Auto) THEN ExRepD)
   THEN (InstLemma `geo-sep-or` [⌜g⌝;⌜a⌝;⌜b⌝;⌜w⌝]⋅ THENA Auto)
   THEN D -1) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. |cd| < |ab|
7. a # b
8. A : Point
9. b-a-A
10. aA ≅ ba
11. w : Point
12. B(Aaw)
13. aw ≅ cd
14. a # w
⊢ ∃w:Point. (B(awb) ∧ aw ≅ cd ∧ w # b)

2
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. |cd| < |ab|
7. a # b
8. A : Point
9. b-a-A
10. aA ≅ ba
11. w : Point
12. B(Aaw)
13. aw ≅ cd
14. b # w
⊢ ∃w:Point. (B(awb) ∧ aw ≅ cd ∧ w # b)

---

Latex:

---

Latex:
No  Annotations
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c,d:Point.    (|cd|  <  |ab|  {}\mRightarrow{}  (\mexists{}w:Point.  (B(awb)  \mwedge{}  aw  \mcong{}  cd  \mwedge{}  w  \#  b)))


By

---

Latex:
(Auto
  THEN  (Assert  a  \#  b  BY
                          (FLemma  `geo-lt-sep`  [-1]  THEN  Auto))
  THEN  ((gProperProlong    \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}`A'\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ExRepD)
  THEN  ((gProlong    \mkleeneopen{}A\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}`w'\mkleeneopen{}c\mkleeneclose{}\mkleeneopen{}d\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ExRepD)
  THEN  (InstLemma  `geo-sep-or`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1)

---

Home Index