---

Step * of Lemma right-angle-SAS

No Annotations
∀e:EuclideanPlane. ∀a,b,c,x,y,z:Point.
  ((Rabc ∧ a # b ∧ b # c) ⇒ (Rxyz ∧ x # y ∧ y # z) ⇒ ab ≅ xy ⇒ bc ≅ yz ⇒ ac ≅ xz)
BY
{ 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. a # b
10. b # c
11. Rxyz
12. x # y
13. y # z
14. ab ≅ xy
15. bc ≅ yz
⊢ ac ≅ xz

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,x,y,z:Point.
    ((Rabc  \mwedge{}  a  \#  b  \mwedge{}  b  \#  c)  {}\mRightarrow{}  (Rxyz  \mwedge{}  x  \#  y  \mwedge{}  y  \#  z)  {}\mRightarrow{}  ab  \mcong{}  xy  {}\mRightarrow{}  bc  \mcong{}  yz  {}\mRightarrow{}  ac  \mcong{}  xz)


By

---

Latex:
Auto

---

Home Index