---

Step * 1 1 3 6 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 eb
24. f leftof be
25. x : Point
26. Colinear(e;b;x)
27. a-x-f
28. x-e-b
⊢ B(exb)
BY
{ ((Assert ⌜False⌝⋅ THEN Auto)
   THEN (((InstLemma `outer-pasch-strict` [⌜g⌝;⌜f⌝;⌜x⌝;⌜a⌝;⌜e⌝;⌜b⌝]⋅ THENA Auto) THEN ExRepD)
         THEN (InstLemma  `adjacent-right-angles-supplementary` [⌜g⌝;⌜b⌝;⌜e⌝;⌜f⌝;⌜p⌝]⋅ THENA Auto)
         )
   THEN D -1
   THEN D -2
   THEN Auto) }

1
.....antecedent..... 
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 eb
24. f leftof be
25. x : Point
26. Colinear(e;b;x)
27. a-x-f
28. x-e-b
29. p : Point
30. f-e-p
31. a-p-b
32. Rbef ⇐ bef ≅a bep
⊢ Rbef

2
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 eb
24. f leftof be
25. x : Point
26. Colinear(e;b;x)
27. a-x-f
28. x-e-b
29. p : Point
30. f-e-p
31. a-p-b
32. Rbef ⇐ bef ≅a bep
33. bef ≅a bep
⊢ False

---

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  eb
24.  f  leftof  be
25.  x  :  Point
26.  Colinear(e;b;x)
27.  a-x-f
28.  x-e-b
\mvdash{}  B(exb)


By

---

Latex:
((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  (((InstLemma  `outer-pasch-strict`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  ExRepD)
              THEN  (InstLemma    `adjacent-right-angles-supplementary`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
              )
  THEN  D  -1
  THEN  D  -2
  THEN  Auto)

---

Home Index