Step * 1 of Lemma cong-angle-out-aux2


1. HeytingGeometry
2. Point
3. Point
4. Point
5. Point
6. Point
7. Point
8. a' Point
9. c' Point
10. d' Point
11. f' Point
12. bc
13. a'c' ≅ d'f'
14. ef
15. out(b a'a)
16. out(b c'c)
17. out(e d'd)
18. out(e f'f)
19. ba' ≅ ed'
20. bc' ≅ ef'
⊢ ∃a',c',x',z':Point. (b_a_a' ∧ b_c_c' ∧ e_d_x' ∧ e_f_z' ∧ ba' ≅ ex' ∧ bc' ≅ ez' ∧ a'c' ≅ x'z')
BY
(((gProperProlong ⌜b⌝⌜a⌝`A'⌜e⌝⌜d⌝⋅ THENA Auto) THEN (gProperProlong ⌜b⌝⌜c⌝`C'⌜e⌝⌜f⌝⋅ THENA Auto))
   THEN (gProperProlong ⌜e⌝⌜d⌝`D'⌜b⌝⌜a⌝⋅ THENA Auto)
   THEN (gProperProlong ⌜e⌝⌜f⌝`F'⌜b⌝⌜c⌝⋅ THENA Auto)
   THEN InstConcl [⌜A⌝;⌜C⌝;⌜D⌝;⌜F⌝]⋅
   THEN Auto) }

1
1. HeytingGeometry
2. Point
3. Point
4. Point
5. Point
6. Point
7. Point
8. a' Point
9. c' Point
10. d' Point
11. f' Point
12. bc
13. a'c' ≅ d'f'
14. ef
15. out(b a'a)
16. out(b c'c)
17. out(e d'd)
18. out(e f'f)
19. ba' ≅ ed'
20. bc' ≅ ef'
21. Point
22. b-a-A
23. aA ≅ ed
24. Point
25. b-c-C
26. cC ≅ ef
27. Point
28. e-d-D
29. dD ≅ ba
30. Point
31. e-f-F
32. fF ≅ bc
33. b_a_A
34. b_c_C
35. e_d_D
36. e_f_F
37. bA ≅ eD
38. bC ≅ eF
⊢ AC ≅ DF


Latex:


Latex:

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  \#  bc
13.  a'c'  \mcong{}  d'f'
14.  d  \#  ef
15.  out(b  a'a)
16.  out(b  c'c)
17.  out(e  d'd)
18.  out(e  f'f)
19.  ba'  \mcong{}  ed'
20.  bc'  \mcong{}  ef'
\mvdash{}  \mexists{}a',c',x',z':Point.  (b\_a\_a'  \mwedge{}  b\_c\_c'  \mwedge{}  e\_d\_x'  \mwedge{}  e\_f\_z'  \mwedge{}  ba'  \mcong{}  ex'  \mwedge{}  bc'  \mcong{}  ez'  \mwedge{}  a'c'  \mcong{}  x'z')


By


Latex:
(((gProperProlong  \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}`A'\mkleeneopen{}e\mkleeneclose{}\mkleeneopen{}d\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  (gProperProlong  \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}`C'\mkleeneopen{}e\mkleeneclose{}\mkleeneopen{}f\mkleeneclose{}\mcdot{}  THENA  Auto))
  THEN  (gProperProlong  \mkleeneopen{}e\mkleeneclose{}\mkleeneopen{}d\mkleeneclose{}`D'\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (gProperProlong  \mkleeneopen{}e\mkleeneclose{}\mkleeneopen{}f\mkleeneclose{}`F'\mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  InstConcl  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}D\mkleeneclose{};\mkleeneopen{}F\mkleeneclose{}]\mcdot{}
  THEN  Auto)




Home Index