---

Step * 1 1 4 4 1 of Lemma rectangle-sides-cong

.....antecedent..... 
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. f : Point
6. e : Point
7. d : Point
8. e # ac
9. d # eb
10. ac  ⊥b be
11. fd  ⊥e eb
12. f-e-d
13. a-b-c
14. ab ≅ eb
15. bc ≅ eb
16. fe ≅ eb
17. ed ≅ eb
18. ae ≅ ce
19. fb ≅ db
20. fb ≅ ae
21. deb ≅a feb
22. abe ≅a cbe
23. a leftof be
24. d leftof be
25. f leftof eb
26. x : Point
27. Colinear(e;b;x)
28. f-x-a
29. e-b-x
30. p : Point
31. a-b-p
32. f-p-e
33. Reba ⇐ eba ≅a ebp
⊢ Reba
BY
{ ((D 10 THEN Auto) THEN InstHyp [⌜a⌝;⌜e⌝] (12)⋅ THEN EAuto 1) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  f  :  Point
6.  e  :  Point
7.  d  :  Point
8.  e  \#  ac
9.  d  \#  eb
10.  ac    \mbot{}b  be
11.  fd    \mbot{}e  eb
12.  f-e-d
13.  a-b-c
14.  ab  \mcong{}  eb
15.  bc  \mcong{}  eb
16.  fe  \mcong{}  eb
17.  ed  \mcong{}  eb
18.  ae  \mcong{}  ce
19.  fb  \mcong{}  db
20.  fb  \mcong{}  ae
21.  deb  \mcong{}\msuba{}  feb
22.  abe  \mcong{}\msuba{}  cbe
23.  a  leftof  be
24.  d  leftof  be
25.  f  leftof  eb
26.  x  :  Point
27.  Colinear(e;b;x)
28.  f-x-a
29.  e-b-x
30.  p  :  Point
31.  a-b-p
32.  f-p-e
33.  Reba  \mLeftarrow{}{}  eba  \mcong{}\msuba{}  ebp
\mvdash{}  Reba


By

---

Latex:
((D  10  THEN  Auto)  THEN  InstHyp  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]  (12)\mcdot{}  THEN  EAuto  1)

---

Home Index