---

Step * 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
⊢ ac ≅ xz
BY
{ ((((InstHyp [⌜c'⌝] (8)⋅ THEN Auto) THENA (D 0 THEN Auto))
    THEN ((InstHyp [⌜z'⌝] (11)⋅ THEN Auto) THENA (D 0 THEN Auto))
    )
   THEN (((InstLemma `Euclid-Prop1` [⌜e⌝;⌜c'⌝;⌜c⌝]⋅ THEN Auto) THEN InstLemma `Euclid-Prop1` [⌜e⌝;⌜z'⌝;⌜z⌝]⋅ THEN Auto)
         THEN ExRepD
         )
   THEN RenameVar `t' (26)) }

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. EQΔ(t;c;c')
28. c1 : Point
29. EQΔ(c1;z;z')
⊢ 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
\mvdash{}  ac  \mcong{}  xz


By

---

Latex:
((((InstHyp  [\mkleeneopen{}c'\mkleeneclose{}]  (8)\mcdot{}  THEN  Auto)  THENA  (D  0  THEN  Auto))
    THEN  ((InstHyp  [\mkleeneopen{}z'\mkleeneclose{}]  (11)\mcdot{}  THEN  Auto)  THENA  (D  0  THEN  Auto))
    )
  THEN  (((InstLemma  `Euclid-Prop1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c'\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THEN  Auto)
                THEN  InstLemma  `Euclid-Prop1`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}z'\mkleeneclose{};\mkleeneopen{}z\mkleeneclose{}]\mcdot{}
                THEN  Auto)
              THEN  ExRepD
              )
  THEN  RenameVar  `t'  (26))

---

Home Index