let x, y be Element of [:REAL,REAL,REAL:]; :: thesis: Eukl_dist3 . (x,y) = Eukl_dist3 . (y,x)
reconsider x1 = x `1_3 , x2 = x `2_3 , x3 = x `3_3 , y1 = y `1_3 , y2 = y `2_3 , y3 = y `3_3 as Element of REAL ;
A1: ( x = [x1,x2,x3] & y = [y1,y2,y3] ) ;
then Eukl_dist3 . (x,y) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2)) by Def22
.= sqrt ((((real_dist . (y1,x1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2)) by METRIC_1:9
.= sqrt ((((real_dist . (y1,x1)) ^2) + ((real_dist . (y2,x2)) ^2)) + ((real_dist . (x3,y3)) ^2)) by METRIC_1:9
.= sqrt ((((real_dist . (y1,x1)) ^2) + ((real_dist . (y2,x2)) ^2)) + ((real_dist . (y3,x3)) ^2)) by METRIC_1:9
.= Eukl_dist3 . (y,x) by A1, Def22 ;
hence Eukl_dist3 . (x,y) = Eukl_dist3 . (y,x) ; :: thesis: verum