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