---

Step * of Lemma interior-angles-unique2

∀e:EuclideanPlane. ∀a,b,c,d,b',c',p:Point.
  (c leftof ab
  ⇒ d leftof ab
  ⇒ p leftof ab
  ⇒ out(a bb')
  ⇒ out(a cc')
  ⇒ b'_p_c'
  ⇒ p ≠ c'
  ⇒ bad < bac
  ⇒ bap ≅a bad
  ⇒ out(a dp))
BY
{ ((Auto THEN (Assert p ≠ a BY (D -1 THEN Auto)))
   THEN ((gProperProlong ⌜p⌝⌜a⌝`q'⌜O⌝⌜X⌝⋅ THENA Auto) THEN ExRepD)
   THEN (((gProperProlong ⌜q⌝⌜a⌝`f'⌜a⌝⌜d⌝⋅ THENA Auto) THEN ExRepD)
         THEN (Assert f leftof ab BY
                     ((InstLemma  `geo-left-out-2` [⌜e⌝;⌜b⌝;⌜a⌝;⌜p⌝;⌜f⌝]⋅ THENA Auto)
                      THEN InstLemma `geo-out-iff-between1` [⌜e⌝;⌜a⌝;⌜p⌝;⌜f⌝;⌜q⌝]⋅
                      THEN Auto))
         )
   THEN InstLemma `Euclid-Prop7` [⌜e⌝;⌜a⌝;⌜b⌝;⌜d⌝;⌜f⌝]⋅
   THEN Auto) }

1
.....antecedent..... 
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. b' : Point
7. c' : Point
8. p : Point
9. c leftof ab
10. d leftof ab
11. p leftof ab
12. out(a bb')
13. out(a cc')
14. b'_p_c'
15. p ≠ c'
16. bad < bac
17. bap ≅a bad
18. p ≠ a
19. q : Point
20. p-a-q
21. aq ≅ OX
22. f : Point
23. q-a-f
24. af ≅ ad
25. f leftof ab
⊢ bd ≅ bf

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. b' : Point
7. c' : Point
8. p : Point
9. c leftof ab
10. d leftof ab
11. p leftof ab
12. out(a bb')
13. out(a cc')
14. b'_p_c'
15. p ≠ c'
16. bad < bac
17. bap ≅a bad
18. p ≠ a
19. q : Point
20. p-a-q
21. aq ≅ OX
22. f : Point
23. q-a-f
24. af ≅ ad
25. f leftof ab
26. d ≡ f
⊢ out(a dp)

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d,b',c',p:Point.
    (c  leftof  ab
    {}\mRightarrow{}  d  leftof  ab
    {}\mRightarrow{}  p  leftof  ab
    {}\mRightarrow{}  out(a  bb')
    {}\mRightarrow{}  out(a  cc')
    {}\mRightarrow{}  b'\_p\_c'
    {}\mRightarrow{}  p  \mneq{}  c'
    {}\mRightarrow{}  bad  <  bac
    {}\mRightarrow{}  bap  \mcong{}\msuba{}  bad
    {}\mRightarrow{}  out(a  dp))


By

---

Latex:
((Auto  THEN  (Assert  p  \mneq{}  a  BY  (D  -1  THEN  Auto)))
  THEN  ((gProperProlong  \mkleeneopen{}p\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}`q'\mkleeneopen{}O\mkleeneclose{}\mkleeneopen{}X\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ExRepD)
  THEN  (((gProperProlong  \mkleeneopen{}q\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}`f'\mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}d\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ExRepD)
              THEN  (Assert  f  leftof  ab  BY
                                      ((InstLemma    `geo-left-out-2`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                        THEN  InstLemma  `geo-out-iff-between1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}
                                        THEN  Auto))
              )
  THEN  InstLemma  `Euclid-Prop7`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index