Step
*
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
⊢ c'c1 ≅ d'd1
BY
{ ((Assert ⌜out(a c'c)⌝⋅ THEN EAuto 1) THEN Assert ⌜out(a cc1)⌝⋅ THEN EAuto 1) }
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)
⊢ 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
\mvdash{}  c'c1  \00D0  d'd1
By
Latex:
((Assert  \mkleeneopen{}out(a  c'c)\mkleeneclose{}\mcdot{}  THEN  EAuto  1)  THEN  Assert  \mkleeneopen{}out(a  cc1)\mkleeneclose{}\mcdot{}  THEN  EAuto  1)
Home
Index