Step
*
1
of Lemma
eu-sum-eq-x
1. e : EuclideanPlane@i'
2. a : Point@i
3. b : Point@i
4. c : Point@i
5. d : Point@i
6. X = |ab| + |cd| ∈ {p:Point| O_X_p} @i
⊢ a = b ∈ Point
BY
{ Assert ⌜X = |ab| ∈ {p:Point| O_X_p} ⌝⋅ }
1
.....assertion.....
1. e : EuclideanPlane@i'
2. a : Point@i
3. b : Point@i
4. c : Point@i
5. d : Point@i
6. X = |ab| + |cd| ∈ {p:Point| O_X_p} @i
⊢ X = |ab| ∈ {p:Point| O_X_p}
2
1. e : EuclideanPlane@i'
2. a : Point@i
3. b : Point@i
4. c : Point@i
5. d : Point@i
6. X = |ab| + |cd| ∈ {p:Point| O_X_p} @i
7. X = |ab| ∈ {p:Point| O_X_p}
⊢ a = b ∈ Point
Latex:
Latex:
1. e : EuclideanPlane@i'
2. a : Point@i
3. b : Point@i
4. c : Point@i
5. d : Point@i
6. X = |ab| + |cd|@i
\mvdash{} a = b
By
Latex:
Assert \mkleeneopen{}X = |ab|\mkleeneclose{}\mcdot{}
Home
Index