---

Step * of Lemma eu-fsc-ap

∀e:EuclideanPlane. ∀a,b,c,d,a',b',c',d':Point.  (FSC(a;b;c;d  a';b';c';d') ⇒ (¬(a = b ∈ Point)) ⇒ cd=c'd')
BY
{ Auto }

1
1. e : EuclideanPlane@i'
2. a : Point@i
3. b : Point@i
4. c : Point@i
5. d : Point@i
6. a' : Point@i
7. b' : Point@i
8. c' : Point@i
9. d' : Point@i
10. FSC(a;b;c;d  a';b';c';d')@i
11. ¬(a = b ∈ Point)@i
⊢ cd=c'd'

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d,a',b',c',d':Point.    (FSC(a;b;c;d    a';b';c';d')  {}\mRightarrow{}  (\mneg{}(a  =  b))  {}\mRightarrow{}  cd=c'd')


By

---

Latex:
Auto

---

Home Index