---

Step * 1 of Lemma geo-CC-2


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)
BY
{ (Assert ∃p,q:Point. ((ab ≅ ap ∧ cd ≥ cp) ∧ cd ≅ cq ∧ ab ≥ aq) BY
         (InstConcl [⌜p⌝;⌜q⌝]⋅ THEN EAuto 1)) }

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
15. ∃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)

---

Latex:

---

Latex:

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  \mcong{}  ap
10.  cd>cp
11.  cd  \mcong{}  cq
12.  ab>aq
13.  CCL(a;b;c;d)  leftof  ac
14.  geo-CCR(g;a;b;c;d)  leftof  ca
\mvdash{}  \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:
(Assert  \mexists{}p,q:Point.  ((ab  \mcong{}  ap  \mwedge{}  cd  \mgeq{}  cp)  \mwedge{}  cd  \mcong{}  cq  \mwedge{}  ab  \mgeq{}  aq)  BY
              (InstConcl  [\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}  THEN  EAuto  1))

---

Home Index