---

Step * of Lemma eu-between-eq-outer-trans

∀e:EuclideanPlane. ∀[a,b,c,d:Point].  (a_c_d) supposing (b_c_d and a_b_c and (¬(b = c ∈ Point)))
BY
{ (Auto
   THEN (Unhide THENA Auto)
   THEN (Assert ¬(a = c ∈ Point) BY
               (ParallelOp 6 THEN (HypSubst' (-1) (-3) THENA Auto) THEN FLemma `eu-between-eq-same` [-3] THEN Auto))
   THEN (Prolong ⌜a⌝ ⌜c⌝ `x' ⌜c⌝ ⌜d⌝⋅ THENA Auto)
   THEN Subst ⌜d = x ∈ Point⌝ 0⋅
   THEN Auto) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. ¬(b = c ∈ Point)
7. a_b_c
8. b_c_d
9. ¬(a = c ∈ Point)
10. x : Point
11. a_c_x
12. cx=cd
⊢ d = x ∈ Point

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (Unhide  THENA  Auto)
  THEN  (Assert  \mneg{}(a  =  c)  BY
                          (ParallelOp  6
                            THEN  (HypSubst'  (-1)  (-3)  THENA  Auto)
                            THEN  FLemma  `eu-between-eq-same`  [-3]
                            THEN  Auto))
  THEN  (Prolong  \mkleeneopen{}a\mkleeneclose{}  \mkleeneopen{}c\mkleeneclose{}  `x'  \mkleeneopen{}c\mkleeneclose{}  \mkleeneopen{}d\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Subst  \mkleeneopen{}d  =  x\mkleeneclose{}  0\mcdot{}
  THEN  Auto)

---

Home Index