the distance of M is symmetric by Def8;
hence for a, b being Element of M holds dist (a,b) = dist (b,a) ; :: thesis: verum