Step
*
of Lemma
cong-angle-out-aux-weak
∀g:HeytingGeometry. ∀a,b,c,d,e,f,a',c',d',f':Point.
(abc ≅a def
⇒ out(b a'a)
⇒ out(b c'c)
⇒ out(e d'd)
⇒ out(e f'f)
⇒ ba' ≅ ed'
⇒ bc' ≅ ef'
⇒ a'c' ≅ d'f')
BY
{ ((Auto THEN D 12 THEN ExRepD)
THEN (Assert out(b a1a') BY
(((Assert out(b aa1) BY
(InstLemma `geo-between-out` [⌜g⌝;⌜b⌝;⌜a⌝;⌜a1⌝]⋅ THEN Auto))
THEN (InstLemma `geo-out_transitivity` [⌜g⌝;⌜b⌝;⌜a'⌝;⌜a⌝;⌜a1⌝]⋅ THENA Auto)
)
THEN EAuto 1
))
) }
1
1. g : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. a' : Point
9. c' : Point
10. d' : Point
11. f' : Point
12. a ≠ b
13. b ≠ c
14. d ≠ e
15. e ≠ f
16. a1 : Point
17. c1 : Point
18. x' : Point
19. z' : Point
20. b_a_a1
21. b_c_c1
22. e_d_x'
23. e_f_z'
24. ba1 ≅ ex'
25. bc1 ≅ ez'
26. a1c1 ≅ x'z'
27. out(b a'a)
28. out(b c'c)
29. out(e d'd)
30. out(e f'f)
31. ba' ≅ ed'
32. bc' ≅ ef'
33. out(b a1a')
⊢ a'c' ≅ d'f'
Latex:
Latex:
\mforall{}g:HeytingGeometry. \mforall{}a,b,c,d,e,f,a',c',d',f':Point.
(abc \mcong{}\msuba{} def
{}\mRightarrow{} out(b a'a)
{}\mRightarrow{} out(b c'c)
{}\mRightarrow{} out(e d'd)
{}\mRightarrow{} out(e f'f)
{}\mRightarrow{} ba' \mcong{} ed'
{}\mRightarrow{} bc' \mcong{} ef'
{}\mRightarrow{} a'c' \mcong{} d'f')
By
Latex:
((Auto THEN D 12 THEN ExRepD)
THEN (Assert out(b a1a') BY
(((Assert out(b aa1) BY
(InstLemma `geo-between-out` [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{}]\mcdot{} THEN Auto))
THEN (InstLemma `geo-out\_transitivity` [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a'\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}a1\mkleeneclose{}]\mcdot{} THENA Auto)
)
THEN EAuto 1
))
)
Home
Index