---

Step * of Lemma Euclid-Prop26-1

∀e:EuclideanPlane. ∀a,b,c,x,y,z:Point.
  (a # bc ⇒ x # yz ⇒ abc ≅a xyz ⇒ bac ≅a yxz ⇒ ab ≅ xy ⇒ (ac ≅ xz ∧ bc ≅ yz ∧ bca ≅a yzx))
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. a # bc
9. x # yz
10. abc ≅a xyz
11. bac ≅a yxz
12. ab ≅ xy
⊢ ac ≅ xz

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a # bc
9. x # yz
10. abc ≅a xyz
11. bac ≅a yxz
12. ab ≅ xy
13. ac ≅ xz
⊢ bc ≅ yz

3
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. y : Point
7. z : Point
8. a # bc
9. x # yz
10. abc ≅a xyz
11. bac ≅a yxz
12. ab ≅ xy
13. ac ≅ xz
14. bc ≅ yz
⊢ bca ≅a yzx

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,x,y,z:Point.
    (a  \#  bc  {}\mRightarrow{}  x  \#  yz  {}\mRightarrow{}  abc  \mcong{}\msuba{}  xyz  {}\mRightarrow{}  bac  \mcong{}\msuba{}  yxz  {}\mRightarrow{}  ab  \mcong{}  xy  {}\mRightarrow{}  (ac  \mcong{}  xz  \mwedge{}  bc  \mcong{}  yz  \mwedge{}  bca  \mcong{}\msuba{}  yzx))


By

---

Latex:
Auto

---

Home Index