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