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