---

Step * 1 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
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)
BY
{ ((Assert BasicGeometryAxioms(g) BY
          ((D 1 THEN Unhide) THEN Auto))
   THEN (InstConcl [⌜CCL(a;b;c;d)⌝;⌜geo-CCR(g;a;b;c;d)⌝]⋅ THEN Auto)
   THEN (((GenConclTerm ⌜CCL(a;b;c;d)⌝⋅ THENA Auto) THEN D -2 THEN Unhide THEN Complete (EAuto 1))
   ORELSE ((GenConclTerm ⌜geo-CCR(g;a;b;c;d)⌝⋅ THENA Auto) THEN D -2 THEN Unhide THEN Complete (EAuto 1))
   )) }

---

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
15.  \mexists{}p,q:Point.  ((ab  \mcong{}  ap  \mwedge{}  cd  \mgeq{}  cp)  \mwedge{}  cd  \mcong{}  cq  \mwedge{}  ab  \mgeq{}  aq)
\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  BasicGeometryAxioms(g)  BY
                ((D  1  THEN  Unhide)  THEN  Auto))
  THEN  (InstConcl  [\mkleeneopen{}CCL(a;b;c;d)\mkleeneclose{};\mkleeneopen{}geo-CCR(g;a;b;c;d)\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  (((GenConclTerm  \mkleeneopen{}CCL(a;b;c;d)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  D  -2  THEN  Unhide  THEN  Complete  (EAuto  1))
  ORELSE  ((GenConclTerm  \mkleeneopen{}geo-CCR(g;a;b;c;d)\mkleeneclose{}\mcdot{}  THENA  Auto)
                  THEN  D  -2
                  THEN  Unhide
                  THEN  Complete  (EAuto  1))
  ))

---

Home Index