---

Step * of Lemma midpoints-preserve-congruence

∀e:BasicGeometry. ∀a,b,c,a',b',c':Point.
  ((((a'=b'=c' ∧ a=b=c) ∧ a' ≠ c' ∧ a ≠ c) ∧ ac ≅ a'c') ⇒ (ab ≅ a'b' ∧ bc ≅ b'c'))
BY
{ Auto }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. b' : Point
7. c' : Point
8. a'=b'=c'
9. a=b=c
10. a' ≠ c'
11. a ≠ c
12. ac ≅ a'c'
⊢ ab ≅ a'b'

2
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. b' : Point
7. c' : Point
8. a'=b'=c'
9. a=b=c
10. a' ≠ c'
11. a ≠ c
12. ac ≅ a'c'
13. ab ≅ a'b'
⊢ bc ≅ b'c'

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,a',b',c':Point.
    ((((a'=b'=c'  \mwedge{}  a=b=c)  \mwedge{}  a'  \mneq{}  c'  \mwedge{}  a  \mneq{}  c)  \mwedge{}  ac  \00D0  a'c')  {}\mRightarrow{}  (ab  \00D0  a'b'  \mwedge{}  bc  \00D0  b'c'))


By

---

Latex:
Auto

---

Home Index