---

Step * 2 1 of Lemma cong-angle-out-exists-iff


1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. b ≠ a
9. b ≠ c
10. y ≠ x
11. y ≠ z
12. a' : Point
13. c' : Point
14. x' : Point
15. z' : Point
16. out(b a'a)
17. out(b c'c)
18. out(y x'x)
19. out(y z'z)
20. a'bc' ≅a x'yz'
⊢ abc ≅a xyz
BY
{ ((D -1 THEN ExRepD)
   THEN (RenameVar `A' (24) THEN RenameVar `C' (25))
   THEN RenameVar `X' (26)
   THEN RenameVar `Z' (27)) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. b ≠ a
9. b ≠ c
10. y ≠ x
11. y ≠ z
12. a' : Point
13. c' : Point
14. x' : Point
15. z' : Point
16. out(b a'a)
17. out(b c'c)
18. out(y x'x)
19. out(y z'z)
20. a' ≠ b
21. b ≠ c'
22. x' ≠ y
23. y ≠ z'
24. A : Point
25. C : Point
26. X : Point
27. Z : Point
28. b_a'_A
29. b_c'_C
30. y_x'_X
31. y_z'_Z
32. bA ≅ yX
33. bC ≅ yZ
34. AC ≅ XZ
⊢ abc ≅a xyz

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  x  :  Point
6.  y  :  Point
7.  z  :  Point
8.  b  \mneq{}  a
9.  b  \mneq{}  c
10.  y  \mneq{}  x
11.  y  \mneq{}  z
12.  a'  :  Point
13.  c'  :  Point
14.  x'  :  Point
15.  z'  :  Point
16.  out(b  a'a)
17.  out(b  c'c)
18.  out(y  x'x)
19.  out(y  z'z)
20.  a'bc'  \mcong{}\msuba{}  x'yz'
\mvdash{}  abc  \mcong{}\msuba{}  xyz


By

---

Latex:
((D  -1  THEN  ExRepD)
  THEN  (RenameVar  `A'  (24)  THEN  RenameVar  `C'  (25))
  THEN  RenameVar  `X'  (26)
  THEN  RenameVar  `Z'  (27))

---

Home Index