---

Step * of Lemma geo-fsc-ap

∀e:BasicGeometry. ∀a,b,c,d,a',b',c',d':Point.  (FSC(a;b;c;d  a';b';c';d') ⇒ a ≠ b ⇒ cd ≅ c'd')
BY
{ Auto }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a' : Point
7. b' : Point
8. c' : Point
9. d' : Point
10. FSC(a;b;c;d  a';b';c';d')
11. a ≠ b
⊢ cd ≅ c'd'

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,d,a',b',c',d':Point.    (FSC(a;b;c;d    a';b';c';d')  {}\mRightarrow{}  a  \mneq{}  b  {}\mRightarrow{}  cd  \00D0  c'd')


By

---

Latex:
Auto

---

Home Index