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 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 ⌜x ∈ Point⌝ 0⋅
   THEN Auto) }

1
1. EuclideanPlane
2. Point
3. Point
4. Point
5. Point
6. ¬(b c ∈ Point)
7. a_b_c
8. b_c_d
9. ¬(a c ∈ Point)
10. Point
11. a_c_x
12. cx=cd
⊢ 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