---

Step * of Lemma out-preserves-lsep

∀g:EuclideanPlane. ∀a,b,c,b',c':Point.  (a # bc ⇒ out(a bb') ⇒ out(a cc') ⇒ a # b'c')
BY
{ (Auto THEN InstLemma `colinear-lsep` [⌜g⌝;⌜b⌝;⌜a⌝;⌜c⌝;⌜b'⌝]⋅ THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c,b',c':Point.    (a  \#  bc  {}\mRightarrow{}  out(a  bb')  {}\mRightarrow{}  out(a  cc')  {}\mRightarrow{}  a  \#  b'c')


By

---

Latex:
(Auto  THEN  InstLemma  `colinear-lsep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b'\mkleeneclose{}]\mcdot{}  THEN  EAuto  1)

---

Home Index