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