---

Step * of Lemma geo-gt-implies-point2

∀e:EuclideanPlane. ∀a,b,c,d:Point.  (ab > cd ⇒ c ≠ d ⇒ (∃f:Point. (c_d_f ∧ cf ≅ ab)))
BY
{ ((Auto THEN (Assert a ≠ b BY (BLemma' `geo-gt-sep` THEN Auto)))
   THEN ((gProperProlong ⌜d⌝⌜c⌝`P'⌜O⌝⌜X⌝⋅ THENA Auto) THEN ExRepD)
   THEN (gProperProlong ⌜P⌝⌜c⌝`f1'⌜a⌝⌜b⌝⋅ THENA Auto)) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. ab > cd
7. c ≠ d
8. a ≠ b
9. P : Point
10. d-c-P
11. cP ≅ OX
12. f1 : Point
13. P-c-f1 ∧ cf1 ≅ ab
⊢ ∃f:Point. (c_d_f ∧ cf ≅ ab)

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d:Point.    (ab  >  cd  {}\mRightarrow{}  c  \mneq{}  d  {}\mRightarrow{}  (\mexists{}f:Point.  (c\_d\_f  \mwedge{}  cf  \mcong{}  ab)))


By

---

Latex:
((Auto  THEN  (Assert  a  \mneq{}  b  BY  (BLemma'  `geo-gt-sep`  THEN  Auto)))
  THEN  ((gProperProlong  \mkleeneopen{}d\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}`P'\mkleeneopen{}O\mkleeneclose{}\mkleeneopen{}X\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ExRepD)
  THEN  (gProperProlong  \mkleeneopen{}P\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}`f1'\mkleeneopen{}a\mkleeneclose{}\mkleeneopen{}b\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index