let M be MetrStruct ; :: thesis: ( ( for a, b being Element of M holds dist a,b = dist b,a ) iff M is symmetric )

hereby :: thesis: ( M is symmetric implies for a, b being Element of M holds dist a,b = dist b,a )

assume A1: for a, b being Element of M holds dist a,b = dist b,a ; :: thesis: M is symmetric
the distance of M is symmetric

proof

let a, b be Element of M; :: according to METRIC_1:def 5 :: thesis: the distance of M . a,b = the distance of M . b,a
thus the distance of M . a,b = dist a,b
.= dist b,a by A1
.= the distance of M . b,a ; :: thesis: verum

end;

hence M is symmetric by Def9; :: thesis: verum

end;

assume M is symmetric ; :: thesis: for a, b being Element of M holds dist a,b = dist b,a
then 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