∀e:BasicGeometry. ∀A,B,C:Point.  (B=A=C 
⇒ (B=A=C ∧ C=A=B))
{ Auto }
1. e : BasicGeometry
2. A : Point
3. B : Point
4. C : Point
5. B=A=C
6. B=A=C
⊢ C=A=B