---

Step * of Lemma geo-CC-2

No Annotations
∀g:EuclideanPlane. ∀a,b,c,d:Point.
  (a # c
  ⇒ (∃p,q:Point. ((ab ≅ ap ∧ cd>cp) ∧ cd ≅ cq ∧ ab>aq))
  ⇒ (∃z1,z2:Point. (az1 ≅ ab ∧ az2 ≅ ab ∧ cz1 ≅ cd ∧ cz2 ≅ cd ∧ z1 leftof ac ∧ z2 leftof ca)))
BY
{ (Auto
   THEN ExRepD
   THEN (InstLemma `geo-CCL-left` [⌜g⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜d⌝]⋅ THENA Auto)
   THEN (InstLemma `geo-CCR-right` [⌜g⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜d⌝]⋅ THENA Auto)) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a # c
7. p : Point
8. q : Point
9. ab ≅ ap
10. cd>cp
11. cd ≅ cq
12. ab>aq
13. CCL(a;b;c;d) leftof ac
14. geo-CCR(g;a;b;c;d) leftof ca
⊢ ∃z1,z2:Point. (az1 ≅ ab ∧ az2 ≅ ab ∧ cz1 ≅ cd ∧ cz2 ≅ cd ∧ z1 leftof ac ∧ z2 leftof ca)

---

Latex:

---

Latex:
No  Annotations
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c,d:Point.
    (a  \#  c
    {}\mRightarrow{}  (\mexists{}p,q:Point.  ((ab  \mcong{}  ap  \mwedge{}  cd>cp)  \mwedge{}  cd  \mcong{}  cq  \mwedge{}  ab>aq))
    {}\mRightarrow{}  (\mexists{}z1,z2:Point.  (az1  \mcong{}  ab  \mwedge{}  az2  \mcong{}  ab  \mwedge{}  cz1  \mcong{}  cd  \mwedge{}  cz2  \mcong{}  cd  \mwedge{}  z1  leftof  ac  \mwedge{}  z2  leftof  ca)))


By

---

Latex:
(Auto
  THEN  ExRepD
  THEN  (InstLemma  `geo-CCL-left`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `geo-CCR-right`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index