---

Step * 1 1 1 of Lemma Euclid-prop16


1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a # bc
7. b-c-d
8. x : {x:Point| b=x=c} 
9. y : {y:Point| a=x=y} 
10. abc ≅a ycb
11. b # x
12. x # c
13. a # x
14. x # y
15. g' : Point
16. a-c-g'
17. cg' ≅ OX
18. x # ac
19. g'-c-a ∧ y-x-a
⊢ cba < acd
BY
{ ((Assert a # xc BY
          ((InstLemma `colinear-lsep` [⌜g⌝;⌜b⌝;⌜c⌝;⌜a⌝;⌜x⌝]⋅ THEN Auto) THEN (D 8 THEN Unhide) THEN EAuto 1))
   THEN (Assert a # yg' ∧ out(a cg') BY
               ((InstLemma `out-preserves-lsep` [⌜g⌝;⌜a⌝;⌜x⌝;⌜c⌝;⌜y⌝;⌜g'⌝]⋅ THEN Auto)
                THEN (InstLemma `geo-between-out` [⌜g⌝;⌜a⌝;⌜x⌝;⌜y⌝]⋅ THEN Auto)
                THEN InstLemma `geo-between-out` [⌜g⌝;⌜a⌝;⌜c⌝;⌜g'⌝]⋅
                THEN Auto))
   ) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a # bc
7. b-c-d
8. x : {x:Point| b=x=c} 
9. y : {y:Point| a=x=y} 
10. abc ≅a ycb
11. b # x
12. x # c
13. a # x
14. x # y
15. g' : Point
16. a-c-g'
17. cg' ≅ OX
18. x # ac
19. g'-c-a ∧ y-x-a
20. a # xc
21. a # yg' ∧ out(a cg')
⊢ cba < acd

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  a  \#  bc
7.  b-c-d
8.  x  :  \{x:Point|  b=x=c\} 
9.  y  :  \{y:Point|  a=x=y\} 
10.  abc  \mcong{}\msuba{}  ycb
11.  b  \#  x
12.  x  \#  c
13.  a  \#  x
14.  x  \#  y
15.  g'  :  Point
16.  a-c-g'
17.  cg'  \mcong{}  OX
18.  x  \#  ac
19.  g'-c-a  \mwedge{}  y-x-a
\mvdash{}  cba  <  acd


By

---

Latex:
((Assert  a  \#  xc  BY
                ((InstLemma  `colinear-lsep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)
                  THEN  (D  8  THEN  Unhide)
                  THEN  EAuto  1))
  THEN  (Assert  a  \#  yg'  \mwedge{}  out(a  cg')  BY
                          ((InstLemma  `out-preserves-lsep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}g'\mkleeneclose{}]\mcdot{}  THEN  Auto)
                            THEN  (InstLemma  `geo-between-out`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THEN  Auto)
                            THEN  InstLemma  `geo-between-out`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}g'\mkleeneclose{}]\mcdot{}
                            THEN  Auto))
  )

---

Home Index