Step
*
of Lemma
geo-left-out-better-1
No Annotations
∀e:EuclideanPlane. ∀a,b,b',p:Point.  (p leftof ba 
⇒ b' # a 
⇒ (¬((¬B(ab'b)) ∧ (¬B(abb')))) 
⇒ p leftof b'a)
BY
{ (Auto
   THEN (Assert p # ba BY
               (OrLeft THEN Auto))
   THEN (Assert Colinear(a;b;b') BY
               (((D 0 THENA Auto) THEN D -3 THEN Auto)
                THEN Try (((D 0 THEN Auto)
                           THEN (Assert Colinear(a;b;b') BY
                                       Auto)
                           THEN Unfold `geo-colinear` -1
                           THEN Auto))
                ))
   THEN (Assert p # b'a BY
               Auto)
   THEN D -1
   THEN Auto
   THEN Assert ⌜False⌝⋅
   THEN Auto) }
1
.....assertion..... 
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. b' : Point
5. p : Point
6. p leftof ba
7. b' # a
8. ¬((¬B(ab'b)) ∧ (¬B(abb')))
9. p # ba
10. Colinear(a;b;b')
11. p leftof ab'
⊢ False
Latex:
Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,b,b',p:Point.
    (p  leftof  ba  {}\mRightarrow{}  b'  \#  a  {}\mRightarrow{}  (\mneg{}((\mneg{}B(ab'b))  \mwedge{}  (\mneg{}B(abb'))))  {}\mRightarrow{}  p  leftof  b'a)
By
Latex:
(Auto
  THEN  (Assert  p  \#  ba  BY
                          (OrLeft  THEN  Auto))
  THEN  (Assert  Colinear(a;b;b')  BY
                          (((D  0  THENA  Auto)  THEN  D  -3  THEN  Auto)
                            THEN  Try  (((D  0  THEN  Auto)
                                                  THEN  (Assert  Colinear(a;b;b')  BY
                                                                          Auto)
                                                  THEN  Unfold  `geo-colinear`  -1
                                                  THEN  Auto))
                            ))
  THEN  (Assert  p  \#  b'a  BY
                          Auto)
  THEN  D  -1
  THEN  Auto
  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
  THEN  Auto)
Home
Index