---

Step * of Lemma congruence-preserves-lsep

∀g:EuclideanPlane. ∀a,b,c,A,B,C:Point.  (ab ≅ AB ⇒ ac ≅ AC ⇒ bc ≅ BC ⇒ c # ab ⇒ (¬¬C # AB))
BY
{ (Auto
   THEN (D 0 THENA Auto)
   THEN (RWO "not-lsep-iff-colinear" (-1) THEN Auto)
   THEN (Assert Colinear(c;a;b) BY
               EasyGeometry)
   THEN RWO "not-lsep-iff-colinear<" (-1)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c,A,B,C:Point.    (ab  \mcong{}  AB  {}\mRightarrow{}  ac  \mcong{}  AC  {}\mRightarrow{}  bc  \mcong{}  BC  {}\mRightarrow{}  c  \#  ab  {}\mRightarrow{}  (\mneg{}\mneg{}C  \#  AB))


By

---

Latex:
(Auto
  THEN  (D  0  THENA  Auto)
  THEN  (RWO  "not-lsep-iff-colinear"  (-1)  THEN  Auto)
  THEN  (Assert  Colinear(c;a;b)  BY
                          EasyGeometry)
  THEN  RWO  "not-lsep-iff-colinear<"  (-1)
  THEN  Auto)

---

Home Index