---

Step * of Lemma Euclid-Prop1-left

No Annotations
∀e:EuclideanPlane. ∀a:Point. ∀b:{b:Point| a # b} .  (∃c:Point [(((cb ≅ ab ∧ ca ≅ ba) ∧ ca ≅ cb) ∧ c leftof ab)])
BY
{ (Auto THEN (CompassCompass2 ⌜a⌝ ⌜b⌝ ⌜b⌝ ⌜a⌝ `c' `d'⋅ THENA Auto)) }

1
.....antecedent..... 
1. e : EuclideanPlane
2. a : Point
3. b : {b:Point| a # b} 
⊢ ∃p,q:Point. ((ab ≅ ap ∧ ba>bp) ∧ ba ≅ bq ∧ ab>aq)

2
1. e : EuclideanPlane
2. a : Point
3. b : {b:Point| a # b} 
4. c : Point
5. d : Point
6. ac ≅ ab ∧ ad ≅ ab ∧ bc ≅ ba ∧ bd ≅ ba ∧ c leftof ab ∧ d leftof ba
⊢ ∃c:Point [(((cb ≅ ab ∧ ca ≅ ba) ∧ ca ≅ cb) ∧ c leftof ab)]

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a:Point.  \mforall{}b:\{b:Point|  a  \#  b\}  .
    (\mexists{}c:Point  [(((cb  \mcong{}  ab  \mwedge{}  ca  \mcong{}  ba)  \mwedge{}  ca  \mcong{}  cb)  \mwedge{}  c  leftof  ab)])


By

---

Latex:
(Auto  THEN  (CompassCompass2  \mkleeneopen{}a\mkleeneclose{}  \mkleeneopen{}b\mkleeneclose{}  \mkleeneopen{}b\mkleeneclose{}  \mkleeneopen{}a\mkleeneclose{}  `c'  `d'\mcdot{}  THENA  Auto))

---

Home Index