---

Step * 1 of Lemma geo-gt-trans


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. x : Point
7. y : Point
8. w1 : Point
9. a_w1_b
10. aw1 ≅ cd
11. w1 ≠ b
12. w : Point
13. c_w_d
14. cw ≅ xy
15. w ≠ d
⊢ ∃w:Point. (a_w_b ∧ aw ≅ xy ∧ w ≠ b)
BY
{ (((InstLemma `geo-congruent-between-exists2` [⌜e⌝;⌜c⌝;⌜w⌝;⌜d⌝;⌜a⌝;⌜w1⌝]⋅ THENA Auto) THEN ExRepD)
   THEN D 0 With ⌜b'⌝ 
   THEN Auto) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. x : Point
7. y : Point
8. w1 : Point
9. a_w1_b
10. aw1 ≅ cd
11. w1 ≠ b
12. w : Point
13. c_w_d
14. cw ≅ xy
15. w ≠ d
16. b' : Point
17. a_b'_w1
18. cw ≅ ab'
19. wd ≅ b'w1
20. a_b'_b
21. ab' ≅ xy
⊢ b' ≠ b

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  x  :  Point
7.  y  :  Point
8.  w1  :  Point
9.  a\_w1\_b
10.  aw1  \mcong{}  cd
11.  w1  \mneq{}  b
12.  w  :  Point
13.  c\_w\_d
14.  cw  \mcong{}  xy
15.  w  \mneq{}  d
\mvdash{}  \mexists{}w:Point.  (a\_w\_b  \mwedge{}  aw  \mcong{}  xy  \mwedge{}  w  \mneq{}  b)


By

---

Latex:
(((InstLemma  `geo-congruent-between-exists2`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}w\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}w1\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  ExRepD)
  THEN  D  0  With  \mkleeneopen{}b'\mkleeneclose{} 
  THEN  Auto)

---

Home Index