---

Step * 2 of Lemma Euclid-Prop1-left


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)]
BY
{ (Auto THEN ThinVar  `d' THEN D 0 With ⌜c⌝  THEN Auto) }

1
1. e : EuclideanPlane
2. a : Point
3. b : {b:Point| a # b} 
4. c : Point
5. ac ≅ ab
6. bc ≅ ba
7. c leftof ab
⊢ cb ≅ ab

2
1. e : EuclideanPlane
2. a : Point
3. b : {b:Point| a # b} 
4. c : Point
5. ac ≅ ab
6. bc ≅ ba
7. c leftof ab
8. cb ≅ ab
⊢ ca ≅ ba

3
1. e : EuclideanPlane
2. a : Point
3. b : {b:Point| a # b} 
4. c : Point
5. ac ≅ ab
6. bc ≅ ba
7. c leftof ab
8. cb ≅ ab
9. ca ≅ ba
⊢ ca ≅ cb

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  \{b:Point|  a  \#  b\} 
4.  c  :  Point
5.  d  :  Point
6.  ac  \mcong{}  ab  \mwedge{}  ad  \mcong{}  ab  \mwedge{}  bc  \mcong{}  ba  \mwedge{}  bd  \mcong{}  ba  \mwedge{}  c  leftof  ab  \mwedge{}  d  leftof  ba
\mvdash{}  \mexists{}c:Point  [(((cb  \mcong{}  ab  \mwedge{}  ca  \mcong{}  ba)  \mwedge{}  ca  \mcong{}  cb)  \mwedge{}  c  leftof  ab)]


By

---

Latex:
(Auto  THEN  ThinVar    `d'  THEN  D  0  With  \mkleeneopen{}c\mkleeneclose{}    THEN  Auto)

---

Home Index