---

Step * 1 1 1 of Lemma right-angle-SAS


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. ∀c':Point. (c'=b=c ⇒ ac ≅ ac')
9. a # b
10. b # c
11. ∀c':Point. (c'=y=z ⇒ xz ≅ xc')
12. x # y
13. y # z
14. ab ≅ xy
15. bc ≅ yz
16. c' : Point
17. c-b-c'
18. bc' ≅ cb
19. z' : Point
20. z-y-z'
21. yz' ≅ zy
22. Rabc
23. Rxyz
24. ac ≅ ac'
25. xz ≅ xz'
26. t : Point
27. EQΔ(t;c;c')
28. c1 : Point
29. EQΔ(c1;z;z')
⊢ ac ≅ xz
BY
{ ((D 29 THEN D 27)
   THEN (InstLemma `upper-dimension-axiom` [⌜e⌝;⌜x⌝;⌜c1⌝;⌜y⌝;⌜z⌝;⌜z'⌝]⋅ THEN Auto)
   THEN InstLemma `upper-dimension-axiom` [⌜e⌝;⌜a⌝;⌜t⌝;⌜b⌝;⌜c⌝;⌜c'⌝]⋅
   THEN Auto) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. ∀c':Point. (c'=b=c ⇒ ac ≅ ac')
9. a # b
10. b # c
11. ∀c':Point. (c'=y=z ⇒ xz ≅ xc')
12. x # y
13. y # z
14. ab ≅ xy
15. bc ≅ yz
16. c' : Point
17. c-b-c'
18. bc' ≅ cb
19. z' : Point
20. z-y-z'
21. yz' ≅ zy
22. Rabc
23. Rxyz
24. ac ≅ ac'
25. xz ≅ xz'
26. t : Point
27. tc ≅ c'c
28. tc' ≅ cc'
29. tc' ≅ tc
30. t # cc'
31. c1 : Point
32. c1z ≅ z'z
33. c1z' ≅ zz'
34. c1z' ≅ c1z
35. c1 # zz'
36. Colinear(x;c1;y)
37. Colinear(a;t;b)
⊢ ac ≅ xz

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  x  :  Point
6.  y  :  Point
7.  z  :  Point
8.  \mforall{}c':Point.  (c'=b=c  {}\mRightarrow{}  ac  \mcong{}  ac')
9.  a  \#  b
10.  b  \#  c
11.  \mforall{}c':Point.  (c'=y=z  {}\mRightarrow{}  xz  \mcong{}  xc')
12.  x  \#  y
13.  y  \#  z
14.  ab  \mcong{}  xy
15.  bc  \mcong{}  yz
16.  c'  :  Point
17.  c-b-c'
18.  bc'  \mcong{}  cb
19.  z'  :  Point
20.  z-y-z'
21.  yz'  \mcong{}  zy
22.  Rabc
23.  Rxyz
24.  ac  \mcong{}  ac'
25.  xz  \mcong{}  xz'
26.  t  :  Point
27.  EQ\mDelta{}(t;c;c')
28.  c1  :  Point
29.  EQ\mDelta{}(c1;z;z')
\mvdash{}  ac  \mcong{}  xz


By

---

Latex:
((D  29  THEN  D  27)
  THEN  (InstLemma  `upper-dimension-axiom`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  InstLemma  `upper-dimension-axiom`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index