---

Step * of Lemma unique-angles-in-half-plane-better2

∀e:EuclideanPlane. ∀a,b,c,q:Point.  (a leftof bc ⇒ q leftof bc ⇒ qcb ≅a acb ⇒ out(c aq))
BY
{ (Auto
   THEN ((gProperProlong ⌜a⌝ ⌜c⌝ `u' ⌜O⌝ ⌜X⌝⋅ THENA Auto) THEN ExRepD)
   THEN (gProperProlong ⌜u⌝ ⌜c⌝ `q1' ⌜c⌝ ⌜q⌝⋅ THENA (Auto THEN D -4 THEN Auto))
   THEN (InstLemma  `Euclid-Prop7` [⌜e⌝;⌜b⌝;⌜c⌝;⌜q⌝;⌜q1⌝]⋅ THENA Auto)) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. q : Point
6. a leftof bc
7. q leftof bc
8. qcb ≅a acb
9. u : Point
10. a-c-u
11. cu ≅ OX
12. q1 : Point
13. u-c-q1
14. cq1 ≅ cq
⊢ q1 ∈ {p:Point| p leftof bc} 

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. q : Point
6. a leftof bc
7. q leftof bc
8. qcb ≅a acb
9. u : Point
10. a-c-u
11. cu ≅ OX
12. q1 : Point
13. u-c-q1
14. cq1 ≅ cq
⊢ bq ≅ bq1

3
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. q : Point
6. a leftof bc
7. q leftof bc
8. qcb ≅a acb
9. u : Point
10. a-c-u
11. cu ≅ OX
12. q1 : Point
13. u-c-q1 ∧ cq1 ≅ cq
14. q ≡ q1
⊢ out(c aq)

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,q:Point.    (a  leftof  bc  {}\mRightarrow{}  q  leftof  bc  {}\mRightarrow{}  qcb  \mcong{}\msuba{}  acb  {}\mRightarrow{}  out(c  aq))


By

---

Latex:
(Auto
  THEN  ((gProperProlong  \mkleeneopen{}a\mkleeneclose{}  \mkleeneopen{}c\mkleeneclose{}  `u'  \mkleeneopen{}O\mkleeneclose{}  \mkleeneopen{}X\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ExRepD)
  THEN  (gProperProlong  \mkleeneopen{}u\mkleeneclose{}  \mkleeneopen{}c\mkleeneclose{}  `q1'  \mkleeneopen{}c\mkleeneclose{}  \mkleeneopen{}q\mkleeneclose{}\mcdot{}  THENA  (Auto  THEN  D  -4  THEN  Auto))
  THEN  (InstLemma    `Euclid-Prop7`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}q1\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index