---

Step * of Lemma use-SC

∀e:EuclideanPlane. ∀a,b,c,d:Point.
  (a ≠ b ⇒ c_b_d ⇒ (∃u,v:Point. (cu ≅ cd ∧ cv ≅ cd ∧ a_b_u ∧ (v_b_u ∧ Colinear(a;b;v)) ∧ (b ≠ d ⇒ v ≠ u))))
BY
{ (Auto
   THEN (InstConcl [⌜SCO(a;b;c;d)⌝;⌜SCS(a;b;c;d)⌝]⋅ THENA Auto)
   THEN (GenConclTerm ⌜SCS(a;b;c;d)⌝⋅ THENA Auto)
   THEN D -2
   THEN Unhide
   THEN Auto
   THEN GenConclTerm ⌜SCO(a;b;c;d)⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d:Point.
    (a  \mneq{}  b
    {}\mRightarrow{}  c\_b\_d
    {}\mRightarrow{}  (\mexists{}u,v:Point.  (cu  \00D0  cd  \mwedge{}  cv  \00D0  cd  \mwedge{}  a\_b\_u  \mwedge{}  (v\_b\_u  \mwedge{}  Colinear(a;b;v))  \mwedge{}  (b  \mneq{}  d  {}\mRightarrow{}  v  \mneq{}  u))))


By

---

Latex:
(Auto
  THEN  (InstConcl  [\mkleeneopen{}SCO(a;b;c;d)\mkleeneclose{};\mkleeneopen{}SCS(a;b;c;d)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (GenConclTerm  \mkleeneopen{}SCS(a;b;c;d)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  D  -2
  THEN  Unhide
  THEN  Auto
  THEN  GenConclTerm  \mkleeneopen{}SCO(a;b;c;d)\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index