---

Step * of Lemma eu-inner-five-segment

∀e:EuclideanPlane
  ∀[a,b,c,d,A,B,C,D:Point].  (bd=BD) supposing (cd=CD and ad=AD and bc=BC and ac=AC and A_B_C and a_b_c)
BY
{ (Auto THEN (Unhide THENA Auto) THEN EuContradiction) }

1
1. e : EuclideanPlane
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. a_b_c
11. A_B_C
12. ac=AC
13. bc=BC
14. ad=AD
15. cd=CD
16. ¬bd=BD
⊢ False

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane
    \mforall{}[a,b,c,d,A,B,C,D:Point].
        (bd=BD)  supposing  (cd=CD  and  ad=AD  and  bc=BC  and  ac=AC  and  A\_B\_C  and  a\_b\_c)


By

---

Latex:
(Auto  THEN  (Unhide  THENA  Auto)  THEN  EuContradiction)

---

Home Index