---

Step * of Lemma sq_stable__geo-left-1

No Annotations
∀g:EuclideanPlaneStructure
  (BasicGeometryAxioms(g) ⇒ (∀a,b,c:Point.  (a # bc ⇒ (¬Colinear(a;b;c)))) ⇒ (∀a,b,c:Point.  SqStable(a leftof bc)))
BY
{ (Auto
   THEN (InstLemma `basic-geo-axioms-imply` [⌜g⌝]⋅ THENA Auto)
   THEN (D 0 THENA Auto)
   THEN (Assert ↓a # bc BY
               (ParallelLast THEN OrLeft THEN Auto))
   THEN (Assert a # bc BY
               (D -1 THEN Unhide THEN Auto))
   THEN D -1
   THEN Auto
   THEN Assert ⌜False⌝⋅
   THEN Auto) }

1
1. g : EuclideanPlaneStructure
2. BasicGeometryAxioms(g)
3. ∀a,b,c:Point.  (a # bc ⇒ (¬Colinear(a;b;c)))
4. a : Point
5. b : Point
6. c : Point
7. ∀a:Point. a ≡ a
8. ∀a,b:Point.  ab ≅ ba
9. ∀a,b,c:Point.  (a ≡ b ⇒ ac ≅ bc)
10. a leftof bc
11. a # bc
12. a leftof cb
⊢ False

---

Latex:

---

Latex:
No  Annotations
\mforall{}g:EuclideanPlaneStructure
    (BasicGeometryAxioms(g)
    {}\mRightarrow{}  (\mforall{}a,b,c:Point.    (a  \#  bc  {}\mRightarrow{}  (\mneg{}Colinear(a;b;c))))
    {}\mRightarrow{}  (\mforall{}a,b,c:Point.    SqStable(a  leftof  bc)))


By

---

Latex:
(Auto
  THEN  (InstLemma  `basic-geo-axioms-imply`  [\mkleeneopen{}g\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  (Assert  \mdownarrow{}a  \#  bc  BY
                          (ParallelLast  THEN  OrLeft  THEN  Auto))
  THEN  (Assert  a  \#  bc  BY
                          (D  -1  THEN  Unhide  THEN  Auto))
  THEN  D  -1
  THEN  Auto
  THEN  Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index