Step
*
1
of Lemma
eu-length-flip
1. e : EuclideanPlane@i'
2. a : Point
3. b : Point
⊢ |ab| = |ba| ∈ Point
BY
{ EAuto 2 }
Latex:
Latex:
1.  e  :  EuclideanPlane@i'
2.  a  :  Point
3.  b  :  Point
\mvdash{}  |ab|  =  |ba|
By
Latex:
EAuto  2
Home
Index