---

Step * 1 1 2 7 1 1 1 1 1 1 1 of Lemma rectangle-sides-cong

.....aux..... 
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. e # ac
9. f # eb
10. ac  ⊥b be
11. df  ⊥e eb
12. d-e-f
13. a-b-c
14. ab ≅ eb
15. bc ≅ eb
16. de ≅ eb
17. ef ≅ eb
18. ae ≅ ce
19. db ≅ fb
20. db ≅ ae
21. feb ≅a deb
22. abe ≅a cbe
23. a leftof be
24. f leftof eb
25. x : Point
26. Colinear(e;b;x)
27. f-x-a
28. B(exb)
29. e # b
30. x # b
31. x # e
32. axb ≅a fxe
33. Reba
34. Rbef
35. xba ≅a xef
36. bx ≅ ex
37. xa ≅ xf
38. xab ≅a xfe
39. fex ≅a dex
40. x # fd
41. fx ≅ dx
42. cbx ≅a abx
43. x # ac
44. cx ≅ ax
45. C : Point
46. d-x-C
47. xC ≅ dx
48. dxf ≅a Cxa
49. fxd ≅a Cxa
50. dxf ≅a axC
51. fxd ≅a axC
52. Cxa ≅a dxf
53. axC ≅a dxf
54. Cxa ≅a fxd
55. axC ≅a fxd
56. Triangle(x;f;d)
⊢ C # a
BY
{ (((Assert x # fd BY Auto) THEN (Assert x # Cf BY Auto)) THEN (Assert a # Cf BY Auto) THEN Auto) }

---

Latex:

---

Latex:
.....aux..... 
1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  e  :  Point
7.  f  :  Point
8.  e  \#  ac
9.  f  \#  eb
10.  ac    \mbot{}b  be
11.  df    \mbot{}e  eb
12.  d-e-f
13.  a-b-c
14.  ab  \mcong{}  eb
15.  bc  \mcong{}  eb
16.  de  \mcong{}  eb
17.  ef  \mcong{}  eb
18.  ae  \mcong{}  ce
19.  db  \mcong{}  fb
20.  db  \mcong{}  ae
21.  feb  \mcong{}\msuba{}  deb
22.  abe  \mcong{}\msuba{}  cbe
23.  a  leftof  be
24.  f  leftof  eb
25.  x  :  Point
26.  Colinear(e;b;x)
27.  f-x-a
28.  B(exb)
29.  e  \#  b
30.  x  \#  b
31.  x  \#  e
32.  axb  \mcong{}\msuba{}  fxe
33.  Reba
34.  Rbef
35.  xba  \mcong{}\msuba{}  xef
36.  bx  \mcong{}  ex
37.  xa  \mcong{}  xf
38.  xab  \mcong{}\msuba{}  xfe
39.  fex  \mcong{}\msuba{}  dex
40.  x  \#  fd
41.  fx  \mcong{}  dx
42.  cbx  \mcong{}\msuba{}  abx
43.  x  \#  ac
44.  cx  \mcong{}  ax
45.  C  :  Point
46.  d-x-C
47.  xC  \mcong{}  dx
48.  dxf  \mcong{}\msuba{}  Cxa
49.  fxd  \mcong{}\msuba{}  Cxa
50.  dxf  \mcong{}\msuba{}  axC
51.  fxd  \mcong{}\msuba{}  axC
52.  Cxa  \mcong{}\msuba{}  dxf
53.  axC  \mcong{}\msuba{}  dxf
54.  Cxa  \mcong{}\msuba{}  fxd
55.  axC  \mcong{}\msuba{}  fxd
56.  Triangle(x;f;d)
\mvdash{}  C  \#  a


By

---

Latex:
(((Assert  x  \#  fd  BY  Auto)  THEN  (Assert  x  \#  Cf  BY  Auto))  THEN  (Assert  a  \#  Cf  BY  Auto)  THEN  Auto)

---

Home Index