---

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


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
15. cb ≅ cb
16. cq ≅ cq1
⊢ bcq ≅a bcq1
BY
{ ((Assert bcq ≅a acb BY
          (FLemma `geo-cong-angle-symmetry` [8] THEN Auto))
   THEN InstLemma  `geo-cong-angle-transitivity` [⌜e⌝;⌜b⌝;⌜c⌝;⌜q⌝;⌜a⌝;⌜c⌝;⌜b⌝;⌜b⌝;⌜c⌝;⌜q1⌝]⋅
   THEN Auto) }

1
.....antecedent..... 
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
15. cb ≅ cb
16. cq ≅ cq1
17. bcq ≅a acb
⊢ acb ≅a bcq1

---

Latex:

---

Latex:

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  \mcong{}\msuba{}  acb
9.  u  :  Point
10.  a-c-u
11.  cu  \mcong{}  OX
12.  q1  :  Point
13.  u-c-q1
14.  cq1  \mcong{}  cq
15.  cb  \mcong{}  cb
16.  cq  \mcong{}  cq1
\mvdash{}  bcq  \mcong{}\msuba{}  bcq1


By

---

Latex:
((Assert  bcq  \mcong{}\msuba{}  acb  BY
                (FLemma  `geo-cong-angle-symmetry`  [8]  THEN  Auto))
  THEN  InstLemma    `geo-cong-angle-transitivity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}q1\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index