Step * 1 of Lemma out-congruent


1. BasicGeometry
2. Point
3. Point
4. Point
5. c' Point
6. c1 Point
7. 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. BasicGeometry
2. Point
3. Point
4. Point
5. c' Point
6. c1 Point
7. 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