let M be MetrStruct ; :: thesis: ( ( for a, b being Element of M holds dist (a,b) = dist (b,a) ) implies M is symmetric )
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 4 :: 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 ; :: thesis: verum