---

Step * 1 of Lemma geo-gt-implies-geo-gt-prim


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. w : Point
7. B(awb)
8. aw ≅ cd
9. w # b
⊢ ab>cd
BY
{ (Assert ab>aw BY
         ((Assert BasicGeometryAxioms(e) BY
                 (D 1 THEN Unhide THEN Auto))
          THEN (Assert ∀a,b,c:Point.  (B(abc) ⇒ b # c ⇒ ac>ab) BY
                      (D -1 THEN SplitAndHyps THEN Auto))
          THEN FHyp (-1) [7]
          THEN Auto)) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. w : Point
7. B(awb)
8. aw ≅ cd
9. w # b
10. ab>aw
⊢ ab>cd

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  w  :  Point
7.  B(awb)
8.  aw  \mcong{}  cd
9.  w  \#  b
\mvdash{}  ab>cd


By

---

Latex:
(Assert  ab>aw  BY
              ((Assert  BasicGeometryAxioms(e)  BY
                              (D  1  THEN  Unhide  THEN  Auto))
                THEN  (Assert  \mforall{}a,b,c:Point.    (B(abc)  {}\mRightarrow{}  b  \#  c  {}\mRightarrow{}  ac>ab)  BY
                                        (D  -1  THEN  SplitAndHyps  THEN  Auto))
                THEN  FHyp  (-1)  [7]
                THEN  Auto))

---

Home Index