---

Step * 1 1 of Lemma out-congruent


1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. c' : Point
6. c1 : Point
7. d : Point
8. d' : Point
9. d1 : Point
10. out(a cc')
11. out(b dd')
12. ac' ≅ bd'
13. a_c_c1
14. b_d_d1
15. cc1 ≅ bd
16. dd1 ≅ ac
17. ac1 ≅ bd1
18. out(a c'c)
19. out(a cc1)
⊢ c'c1 ≅ d'd1
BY
{ (InstLemma `geo-out_transitivity` [⌜e⌝;⌜a⌝;⌜c'⌝;⌜c⌝;⌜c1⌝]⋅ THENA Auto) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. c' : Point
6. c1 : Point
7. d : Point
8. d' : Point
9. d1 : Point
10. out(a cc')
11. out(b dd')
12. ac' ≅ bd'
13. a_c_c1
14. b_d_d1
15. cc1 ≅ bd
16. dd1 ≅ ac
17. ac1 ≅ bd1
18. out(a c'c)
19. out(a cc1)
20. out(a c'c1)
⊢ c'c1 ≅ d'd1

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  c'  :  Point
6.  c1  :  Point
7.  d  :  Point
8.  d'  :  Point
9.  d1  :  Point
10.  out(a  cc')
11.  out(b  dd')
12.  ac'  \00D0  bd'
13.  a\_c\_c1
14.  b\_d\_d1
15.  cc1  \00D0  bd
16.  dd1  \00D0  ac
17.  ac1  \00D0  bd1
18.  out(a  c'c)
19.  out(a  cc1)
\mvdash{}  c'c1  \00D0  d'd1


By

---

Latex:
(InstLemma  `geo-out\_transitivity`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index