---

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

.....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. qbc ≅a abc
9. u : Point
10. a-b-u
11. bu ≅ OX
12. q1 : Point
13. u-b-q1
14. bq1 ≅ bq
15. bc ≅ bc
16. bq ≅ bq1
17. cbq ≅a abc
⊢ abc ≅a cbq1
BY
{ (InstLemma  `out-preserves-angle-cong_1` [⌜e⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜q1⌝;⌜c⌝;⌜a⌝;⌜c⌝]⋅ THEN EAuto 1) }

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. qbc ≅a abc
9. u : Point
10. a-b-u
11. bu ≅ OX
12. q1 : Point
13. u-b-q1
14. bq1 ≅ bq
15. bc ≅ bc
16. bq ≅ bq1
17. cbq ≅a abc
⊢ out(b aq1)

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. qbc ≅a abc
9. u : Point
10. a-b-u
11. bu ≅ OX
12. q1 : Point
13. u-b-q1
14. bq1 ≅ bq
15. bc ≅ bc
16. bq ≅ bq1
17. cbq ≅a abc
18. q1bc ≅a abc
⊢ abc ≅a cbq1

---

Latex:

---

Latex:
.....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.  qbc  \mcong{}\msuba{}  abc
9.  u  :  Point
10.  a-b-u
11.  bu  \mcong{}  OX
12.  q1  :  Point
13.  u-b-q1
14.  bq1  \mcong{}  bq
15.  bc  \mcong{}  bc
16.  bq  \mcong{}  bq1
17.  cbq  \mcong{}\msuba{}  abc
\mvdash{}  abc  \mcong{}\msuba{}  cbq1


By

---

Latex:
(InstLemma    `out-preserves-angle-cong\_1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}q1\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}
  THEN  EAuto  1
  )

---

Home Index