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