---

Step * of Lemma out-congruent

∀e:BasicGeometry. ∀a,b,c,c',c1,d,d',d1:Point.
  (out(a cc') ⇒ out(b dd') ⇒ ac' ≅ bd' ⇒ a_c_c1 ⇒ b_d_d1 ⇒ cc1 ≅ bd ⇒ dd1 ≅ ac ⇒ (ac1 ≅ bd1 ∧ c'c1 ≅ d'd1))
BY
{ Auto }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. c' : Point
6. c1 : Point
7. d : Point
8. d' : Point
9. d1 : Point
10. out(a cc')
11. out(b dd')
12. ac' ≅ bd'
13. a_c_c1
14. b_d_d1
15. cc1 ≅ bd
16. dd1 ≅ ac
17. ac1 ≅ bd1
⊢ c'c1 ≅ d'd1

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,c',c1,d,d',d1:Point.
    (out(a  cc')
    {}\mRightarrow{}  out(b  dd')
    {}\mRightarrow{}  ac'  \00D0  bd'
    {}\mRightarrow{}  a\_c\_c1
    {}\mRightarrow{}  b\_d\_d1
    {}\mRightarrow{}  cc1  \00D0  bd
    {}\mRightarrow{}  dd1  \00D0  ac
    {}\mRightarrow{}  (ac1  \00D0  bd1  \mwedge{}  c'c1  \00D0  d'd1))


By

---

Latex:
Auto

---

Home Index