---

Step * of Lemma eu-five-segment

∀e:EuclideanPlane
  ∀[a,b,c,d,A,B,C,D:Point].
    (cd=CD) supposing (bd=BD and ad=AD and bc=BC and ab=AB and A_B_C and a_b_c and (¬(a = b ∈ Point)))
BY
{ ((D 0 THENA Auto) THEN D 1 THEN (Unhide THENA Auto) THEN (D 2 THEN SplitAndHyps) THEN Trivial) }

---

Latex:

---

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


By

---

Latex:
((D  0  THENA  Auto)  THEN  D  1  THEN  (Unhide  THENA  Auto)  THEN  (D  2  THEN  SplitAndHyps)  THEN  Trivial)

---

Home Index