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

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

hence
M is symmetric
; :: thesis: verum
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;thus the distance of M . (a,b) = dist (a,b)

.= dist (b,a) by A1

.= the distance of M . (b,a) ; :: thesis: verum