---

Step * of Lemma sq_stable__geo-left

∀g:EuclideanPlane. ∀a,b,c:Point.  SqStable(a leftof bc)
BY
{ ((D 0 THENA Auto) THEN (InstLemma `sq_stable__geo-left-1` [⌜g⌝]⋅ THENM Trivial)) }

1
.....wf..... 
1. g : EuclideanPlane
⊢ g ∈ EuclideanPlaneStructure

2
.....antecedent..... 
1. g : EuclideanPlane
⊢ BasicGeometryAxioms(g)

3
.....antecedent..... 
1. g : EuclideanPlane
⊢ ∀a,b,c:Point.  (a # bc ⇒ (¬Colinear(a;b;c)))

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c:Point.    SqStable(a  leftof  bc)


By

---

Latex:
((D  0  THENA  Auto)  THEN  (InstLemma  `sq\_stable\_\_geo-left-1`  [\mkleeneopen{}g\mkleeneclose{}]\mcdot{}  THENM  Trivial))

---

Home Index