---

Step * of Lemma geo-right-angles-congruent

∀e:EuclideanPlane. ∀a,b,c,x,y,z:Point.  (((Rabc ∧ Rxyz) ∧ (x ≠ y ∧ y ≠ z) ∧ a ≠ b ∧ b ≠ c) ⇒ abc ≅a xyz)
BY
{ (Auto THEN (gProperProlong ⌜b⌝⌜a⌝`A'⌜y⌝⌜x⌝⋅ THEN Auto) THEN gProperProlong ⌜b⌝⌜c⌝`C'⌜y⌝⌜z⌝⋅ 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. Rabc
9. Rxyz
10. x ≠ y
11. y ≠ z
12. a ≠ b
13. b ≠ c
14. A : Point
15. b-a-A
16. aA ≅ yx
17. C : Point
18. b-c-C
19. cC ≅ yz
⊢ abc ≅a xyz

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,x,y,z:Point.
    (((Rabc  \mwedge{}  Rxyz)  \mwedge{}  (x  \mneq{}  y  \mwedge{}  y  \mneq{}  z)  \mwedge{}  a  \mneq{}  b  \mwedge{}  b  \mneq{}  c)  {}\mRightarrow{}  abc  \mcong{}\msuba{}  xyz)


By

---

Latex:
(Auto
  THEN  (gProperProlong  \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}a\mkleeneclose{}`A'\mkleeneopen{}y\mkleeneclose{}\mkleeneopen{}x\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  gProperProlong  \mkleeneopen{}b\mkleeneclose{}\mkleeneopen{}c\mkleeneclose{}`C'\mkleeneopen{}y\mkleeneclose{}\mkleeneopen{}z\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index