---

Step * 2 2 of Lemma geo-lt-implies-gt-strong-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. b # w
15. Colinear(a;w;b)
16. w-b-a
⊢ B(awb)
BY
{ (((Assert B(abw) BY Auto) THEN (FLemma `geo-le-from-be` [-1] THENA Auto))
   THEN (FLemma `geo-le_weakening-lt` [6] THENA Auto)
   THEN ((Assert |cd| = |ab| ∈ Length BY
                Auto)
         THENA ((Assert cd ≅ ab BY InstLemma `geo-le-congruent` [⌜g⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜d⌝]⋅) THEN Auto)
         )
   THEN (RWO "-1" (6) THEN Auto)
   THEN FLemma `geo-lt-irrefl` [6]
   THEN Auto) }

---

Latex:

---

Latex:

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  \mcong{}  ba
11.  w  :  Point
12.  B(Aaw)
13.  aw  \mcong{}  cd
14.  b  \#  w
15.  Colinear(a;w;b)
16.  w-b-a
\mvdash{}  B(awb)


By

---

Latex:
(((Assert  B(abw)  BY  Auto)  THEN  (FLemma  `geo-le-from-be`  [-1]  THENA  Auto))
  THEN  (FLemma  `geo-le\_weakening-lt`  [6]  THENA  Auto)
  THEN  ((Assert  |cd|  =  |ab|  BY
                            Auto)
              THENA  ((Assert  cd  \mcong{}  ab  BY  InstLemma  `geo-le-congruent`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{})  THEN  Auto)
              )
  THEN  (RWO  "-1"  (6)  THEN  Auto)
  THEN  FLemma  `geo-lt-irrefl`  [6]
  THEN  Auto)

---

Home Index