---

Step * of Lemma eu-between-eq-exchange4

∀e:EuclideanPlane. ∀[a,b,c,d:Point].  (a_b_d) supposing (a_c_d and a_b_c)
BY
{ ((Auto THEN (Unhide THENA Auto))
   THEN EuContradiction
   THEN (Assert ¬(b = c ∈ Point) BY
               (ParallelLast THEN Auto))
   THEN D -2) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a_b_c
7. a_c_d
8. ¬(b = c ∈ Point)
⊢ a_b_d

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}[a,b,c,d:Point].    (a\_b\_d)  supposing  (a\_c\_d  and  a\_b\_c)


By

---

Latex:
((Auto  THEN  (Unhide  THENA  Auto))
  THEN  EuContradiction
  THEN  (Assert  \mneg{}(b  =  c)  BY
                          (ParallelLast  THEN  Auto))
  THEN  D  -2)

---

Home Index