∀e:EuclideanPlane. ∀[a,b,c,d:Point]. cd=ab supposing ab=cd
{ (Auto THEN (Assert e ∈ EuclideanPlane BY Auto)) }
1. e : EuclideanPlane@i'
2. [a] : Point
3. [b] : Point
4. [c] : Point
5. [d] : Point
6. [%] : ab=cd
7. e ∈ EuclideanPlane
⊢ cd=ab