---

Step * of Lemma geo-out-cong-cong

∀e:BasicGeometry. ∀a,b,c,a',b',c':Point.  (out(a bc) ⇒ out(a' b'c') ⇒ ab ≅ a'b' ⇒ ac ≅ a'c' ⇒ 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. out(a bc)
9. out(a' b'c')
10. ab ≅ a'b'
11. ac ≅ a'c'
⊢ bc ≅ b'c'

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index