---

Step * of Lemma parallelogram-construction

No Annotations
∀e:EuclideanPlane. ∀a,b,c,x,y:Point.
  (a # bc
  ⇒ a-x-b
  ⇒ a-y-c
  ⇒ (∃t:Point
       (geo-parallel-points(e;b;x;y;t)
       ∧ (¬¬((a leftof bc ⇒ (t leftof ac ∧ t leftof bc)) ∧ (a leftof cb ⇒ (t leftof ca ∧ t leftof cb)))))))
BY
{ (InstLemma `parallelogram-construction2` [] THEN RepeatFor 10 ((ParallelLast' THENA Auto)) THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,x,y:Point.
    (a  \#  bc
    {}\mRightarrow{}  a-x-b
    {}\mRightarrow{}  a-y-c
    {}\mRightarrow{}  (\mexists{}t:Point
              (geo-parallel-points(e;b;x;y;t)
              \mwedge{}  (\mneg{}\mneg{}((a  leftof  bc  {}\mRightarrow{}  (t  leftof  ac  \mwedge{}  t  leftof  bc))
                  \mwedge{}  (a  leftof  cb  {}\mRightarrow{}  (t  leftof  ca  \mwedge{}  t  leftof  cb)))))))


By

---

Latex:
(InstLemma  `parallelogram-construction2`  []
  THEN  RepeatFor  10  ((ParallelLast'  THENA  Auto))
  THEN  Auto)

---

Home Index